Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem fodom 3613

Description: An onto function implies dominance of range over domain. Lemma 10.20 of [Kunen] p. 30. This theorem uses the Axiom of Choice ac7g 3570.

**Hypothesis**
Ref	Expression
fodom.1	⊢ A ∈ V

**Assertion**
Ref	Expression
fodom	⊢ (F:A–onto→B → B ≼ A)

**Proof of Theorem fodom**
Step	Hyp	Ref	Expression
1		fof 2788	. . . 4 ⊢ (F:A–onto→B → F:A–→B)
2		fodom.1	. . . . 5 ⊢ A ∈ V
3		fex 2771	. . . . 5 ⊢ (A ∈ V → (F:A–→B → F ∈ V))
4	2, 3	ax-mp 6	. . . 4 ⊢ (F:A–→B → F ∈ V)
5	1, 4	syl 12	. . 3 ⊢ (F:A–onto→B → F ∈ V)
6		cnvexg 2669	. . 3 ⊢ (F ∈ V → ^◡F ∈ V)
7		ac7g 3570	. . 3 ⊢ (^◡F ∈ V → ∃f(f ⊆ ^◡F ∧ f Fn dom ^◡F))
8	5, 6, 7	3syl 21	. 2 ⊢ (F:A–onto→B → ∃f(f ⊆ ^◡F ∧ f Fn dom ^◡F))
9		forn 2789	. . . . . . . 8 ⊢ (F:A–onto→B → ran F = B)
10		df-rn 2429	. . . . . . . 8 ⊢ ran F = dom ^◡F
11	9, 10	syl5eqr 1138	. . . . . . 7 ⊢ (F:A–onto→B → dom ^◡F = B)
12		fneq2 2719	. . . . . . 7 ⊢ (dom ^◡F = B → (f Fn dom ^◡F ↔ f Fn B))
13	11, 12	syl 12	. . . . . 6 ⊢ (F:A–onto→B → (f Fn dom ^◡F ↔ f Fn B))
14		domtr 3320	. . . . . . . 8 ⊢ ((B ≼ ran f ∧ ran f ≼ A) → B ≼ A)
15		fnfrn 2758	. . . . . . . . . . . . 13 ⊢ (f Fn B ↔ f:B–→ran f)
16	15	biimp 133	. . . . . . . . . . . 12 ⊢ (f Fn B → f:B–→ran f)
17	16	ad2antlr 321	. . . . . . . . . . 11 ⊢ (((F:A–onto→B ∧ f Fn B) ∧ f ⊆ ^◡F) → f:B–→ran f)
18		funss 2682	. . . . . . . . . . . . . . 15 ⊢ (^◡f ⊆ F → (Fun F → Fun ^◡f))
19	18	com12 13	. . . . . . . . . . . . . 14 ⊢ (Fun F → (^◡f ⊆ F → Fun ^◡f))
20	19	imp 277	. . . . . . . . . . . . 13 ⊢ ((Fun F ∧ ^◡f ⊆ F) → Fun ^◡f)
21		ffun 2754	. . . . . . . . . . . . . 14 ⊢ (F:A–→B → Fun F)
22	1, 21	syl 12	. . . . . . . . . . . . 13 ⊢ (F:A–onto→B → Fun F)
23		cnvss 2512	. . . . . . . . . . . . . 14 ⊢ (f ⊆ ^◡F → ^◡f ⊆ ^◡^◡F)
24		cnvcnvss 2662	. . . . . . . . . . . . . . 15 ⊢ ^◡^◡F ⊆ F
25		sstr 1511	. . . . . . . . . . . . . . 15 ⊢ ((^◡f ⊆ ^◡^◡F ∧ ^◡^◡F ⊆ F) → ^◡f ⊆ F)
26	24, 25	mpan2 519	. . . . . . . . . . . . . 14 ⊢ (^◡f ⊆ ^◡^◡F → ^◡f ⊆ F)
27	23, 26	syl 12	. . . . . . . . . . . . 13 ⊢ (f ⊆ ^◡F → ^◡f ⊆ F)
28	20, 22, 27	syl2an 349	. . . . . . . . . . . 12 ⊢ ((F:A–onto→B ∧ f ⊆ ^◡F) → Fun ^◡f)
29	28	adantlr 310	. . . . . . . . . . 11 ⊢ (((F:A–onto→B ∧ f Fn B) ∧ f ⊆ ^◡F) → Fun ^◡f)
30	17, 29	jca 236	. . . . . . . . . 10 ⊢ (((F:A–onto→B ∧ f Fn B) ∧ f ⊆ ^◡F) → (f:B–→ran f ∧ Fun ^◡f))
31		df-f1 2435	. . . . . . . . . 10 ⊢ (f:B–1-1→ran f ↔ (f:B–→ran f ∧ Fun ^◡f))
32	30, 31	sylibr 175	. . . . . . . . 9 ⊢ (((F:A–onto→B ∧ f Fn B) ∧ f ⊆ ^◡F) → f:B–1-1→ran f)
33		visset 1350	. . . . . . . . . . 11 ⊢ f ∈ V
34		rnexg 2569	. . . . . . . . . . 11 ⊢ (f ∈ V → ran f ∈ V)
35	33, 34	ax-mp 6	. . . . . . . . . 10 ⊢ ran f ∈ V
36		f1dom2g 3300	. . . . . . . . . 10 ⊢ (ran f ∈ V → (f:B–1-1→ran f → B ≼ ran f))
37	35, 36	ax-mp 6	. . . . . . . . 9 ⊢ (f:B–1-1→ran f → B ≼ ran f)
38	32, 37	syl 12	. . . . . . . 8 ⊢ (((F:A–onto→B ∧ f Fn B) ∧ f ⊆ ^◡F) → B ≼ ran f)
39		rnss 2558	. . . . . . . . . . . 12 ⊢ (f ⊆ ^◡F → ran f ⊆ ran ^◡F)
40	39	adantl 305	. . . . . . . . . . 11 ⊢ ((F:A–onto→B ∧ f ⊆ ^◡F) → ran f ⊆ ran ^◡F)
41		fdm 2756	. . . . . . . . . . . . . 14 ⊢ (F:A–→B → dom F = A)
42	1, 41	syl 12	. . . . . . . . . . . . 13 ⊢ (F:A–onto→B → dom F = A)
43		dfdm4 2525	. . . . . . . . . . . . 13 ⊢ dom F = ran ^◡F
44	42, 43	syl5eqr 1138	. . . . . . . . . . . 12 ⊢ (F:A–onto→B → ran ^◡F = A)
45	44	adantr 306	. . . . . . . . . . 11 ⊢ ((F:A–onto→B ∧ f ⊆ ^◡F) → ran ^◡F = A)
46	40, 45	sseqtrd 1536	. . . . . . . . . 10 ⊢ ((F:A–onto→B ∧ f ⊆ ^◡F) → ran f ⊆ A)
47		ssdomg 3311	. . . . . . . . . . 11 ⊢ (ran f ∈ V → (ran f ⊆ A → ran f ≼ A))
48	35, 47	ax-mp 6	. . . . . . . . . 10 ⊢ (ran f ⊆ A → ran f ≼ A)
49	46, 48	syl 12	. . . . . . . . 9 ⊢ ((F:A–onto→B ∧ f ⊆ ^◡F) → ran f ≼ A)
50	49	adantlr 310	. . . . . . . 8 ⊢ (((F:A–onto→B ∧ f Fn B) ∧ f ⊆ ^◡F) → ran f ≼ A)
51	14, 38, 50	sylanc 361	. . . . . . 7 ⊢ (((F:A–onto→B ∧ f Fn B) ∧ f ⊆ ^◡F) → B ≼ A)
52	51	exp31 293	. . . . . 6 ⊢ (F:A–onto→B → (f Fn B → (f ⊆ ^◡F → B ≼ A)))
53	13, 52	sylbid 178	. . . . 5 ⊢ (F:A–onto→B → (f Fn dom ^◡F → (f ⊆ ^◡F → B ≼ A)))
54	53	com23 32	. . . 4 ⊢ (F:A–onto→B → (f ⊆ ^◡F → (f Fn dom ^◡F → B ≼ A)))
55	54	imp3a 279	. . 3 ⊢ (F:A–onto→B → ((f ⊆ ^◡F ∧ f Fn dom ^◡F) → B ≼ A))
56	55	19.23adv 954	. 2 ⊢ (F:A–onto→B → (∃f(f ⊆ ^◡F ∧ f Fn dom ^◡F) → B ≼ A))
57	8, 56	mpd 46	1 ⊢ (F:A–onto→B → B ≼ A)

Colors of variables: wff set class

Syntax hints: → wi 2 ↔ wb 127 ∧ wa 196 ∃wex 678 = wceq 1091 ∈ wcel 1092 Vcvv 1348 ⊆ wss 1487 class class class wbr 2054 ^◡ccnv 2409 dom cdm 2410 ran crn 2411 Fun wfun 2416 Fn wfn 2417 –→wf 2418 –1-1→wf1 2419 –onto→wfo 2420 ≼ cdom 3272

This theorem is referenced by: fodomg 3614 fodomb 3615 qnnen 4931

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-ac 1080

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-op 1815 df-uni 1920 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-fr 2169 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-en 3274 df-dom 3275

metamath.org