Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem fodomb 3615

Description: Equivalence of an onto mapping and dominance for a non-empty set. Proposition 10.35 of [TakeutiZaring] p. 93.

**Hypotheses**
Ref	Expression
fodomb.1	⊢ A ∈ V
fodomb.2	⊢ B ∈ V

**Assertion**
Ref	Expression
fodomb	⊢ ((¬ A = ∅ ∧ ∃f f:A–onto→B) ↔ (∅ ≺ B ∧ B ≼ A))

Distinct variable group(s): A,f B,f

**Proof of Theorem fodomb**
Step	Hyp	Ref	Expression
1		fof 2788	. . . . . . . . . . 11 ⊢ (f:A–onto→B → f:A–→B)
2		fdm 2756	. . . . . . . . . . 11 ⊢ (f:A–→B → dom f = A)
3	1, 2	syl 12	. . . . . . . . . 10 ⊢ (f:A–onto→B → dom f = A)
4	3	cleq1d 1109	. . . . . . . . 9 ⊢ (f:A–onto→B → (dom f = ∅ ↔ A = ∅))
5		forn 2789	. . . . . . . . . . 11 ⊢ (f:A–onto→B → ran f = B)
6	5	cleq1d 1109	. . . . . . . . . 10 ⊢ (f:A–onto→B → (ran f = ∅ ↔ B = ∅))
7		dm0rn0 2549	. . . . . . . . . 10 ⊢ (dom f = ∅ ↔ ran f = ∅)
8	6, 7	syl5bb 410	. . . . . . . . 9 ⊢ (f:A–onto→B → (dom f = ∅ ↔ B = ∅))
9	4, 8	bitr3d 408	. . . . . . . 8 ⊢ (f:A–onto→B → (A = ∅ ↔ B = ∅))
10	9	negbid 463	. . . . . . 7 ⊢ (f:A–onto→B → (¬ A = ∅ ↔ ¬ B = ∅))
11	10	biimpcd 137	. . . . . 6 ⊢ (¬ A = ∅ → (f:A–onto→B → ¬ B = ∅))
12		fodomb.2	. . . . . . 7 ⊢ B ∈ V
13	12	0sdom 3368	. . . . . 6 ⊢ (∅ ≺ B ↔ ¬ B = ∅)
14	11, 13	syl6ibr 186	. . . . 5 ⊢ (¬ A = ∅ → (f:A–onto→B → ∅ ≺ B))
15		fodomb.1	. . . . . . 7 ⊢ A ∈ V
16	15	fodom 3613	. . . . . 6 ⊢ (f:A–onto→B → B ≼ A)
17	16	a1i 7	. . . . 5 ⊢ (¬ A = ∅ → (f:A–onto→B → B ≼ A))
18	14, 17	jcad 455	. . . 4 ⊢ (¬ A = ∅ → (f:A–onto→B → (∅ ≺ B ∧ B ≼ A)))
19	18	19.23adv 954	. . 3 ⊢ (¬ A = ∅ → (∃f f:A–onto→B → (∅ ≺ B ∧ B ≼ A)))
20	19	imp 277	. 2 ⊢ ((¬ A = ∅ ∧ ∃f f:A–onto→B) → (∅ ≺ B ∧ B ≼ A))
21		sdomdomtr 3370	. . . . 5 ⊢ (A ∈ V → ((∅ ≺ B ∧ B ≼ A) → ∅ ≺ A))
22	15, 21	ax-mp 6	. . . 4 ⊢ ((∅ ≺ B ∧ B ≼ A) → ∅ ≺ A)
23	15	0sdom 3368	. . . 4 ⊢ (∅ ≺ A ↔ ¬ A = ∅)
24	22, 23	sylib 173	. . 3 ⊢ ((∅ ≺ B ∧ B ≼ A) → ¬ A = ∅)
25		df-f1 2435	. . . . . . . . . . . . . . . . 17 ⊢ (g:B–1-1→A ↔ (g:B–→A ∧ Fun ^◡g))
26	25	pm3.27bd 263	. . . . . . . . . . . . . . . 16 ⊢ (g:B–1-1→A → Fun ^◡g)
27		visset 1350	. . . . . . . . . . . . . . . . . 18 ⊢ z ∈ V
28	27	fconst 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((A ∖ ran g) × {z}):(A ∖ ran g)–→{z}
29		ffun 2754	. . . . . . . . . . . . . . . . 17 ⊢ (((A ∖ ran g) × {z}):(A ∖ ran g)–→{z} → Fun ((A ∖ ran g) × {z}))
30	28, 29	ax-mp 6	. . . . . . . . . . . . . . . 16 ⊢ Fun ((A ∖ ran g) × {z})
31	26, 30	jctir 241	. . . . . . . . . . . . . . 15 ⊢ (g:B–1-1→A → (Fun ^◡g ∧ Fun ((A ∖ ran g) × {z})))
32		df-rn 2429	. . . . . . . . . . . . . . . . . . 19 ⊢ ran g = dom ^◡g
33	32	cleqcomi 1105	. . . . . . . . . . . . . . . . . 18 ⊢ dom ^◡g = ran g
34	27	snnz 1846	. . . . . . . . . . . . . . . . . . 19 ⊢ ¬ {z} = ∅
35		dmxp 2552	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ {z} = ∅ → dom ((A ∖ ran g) × {z}) = (A ∖ ran g))
36	34, 35	ax-mp 6	. . . . . . . . . . . . . . . . . 18 ⊢ dom ((A ∖ ran g) × {z}) = (A ∖ ran g)
37	33, 36	ineq12i 1643	. . . . . . . . . . . . . . . . 17 ⊢ (dom ^◡g ∩ dom ((A ∖ ran g) × {z})) = (ran g ∩ (A ∖ ran g))
38		difdisj 1758	. . . . . . . . . . . . . . . . 17 ⊢ (ran g ∩ (A ∖ ran g)) = ∅
39	37, 38	eqtr 1119	. . . . . . . . . . . . . . . 16 ⊢ (dom ^◡g ∩ dom ((A ∖ ran g) × {z})) = ∅
40		funun 2700	. . . . . . . . . . . . . . . 16 ⊢ (((Fun ^◡g ∧ Fun ((A ∖ ran g) × {z})) ∧ (dom ^◡g ∩ dom ((A ∖ ran g) × {z})) = ∅) → Fun (^◡g ∪ ((A ∖ ran g) × {z})))
41	39, 40	mpan2 519	. . . . . . . . . . . . . . 15 ⊢ ((Fun ^◡g ∧ Fun ((A ∖ ran g) × {z})) → Fun (^◡g ∪ ((A ∖ ran g) × {z})))
42	31, 41	syl 12	. . . . . . . . . . . . . 14 ⊢ (g:B–1-1→A → Fun (^◡g ∪ ((A ∖ ran g) × {z})))
43	42	adantl 305	. . . . . . . . . . . . 13 ⊢ ((z ∈ B ∧ g:B–1-1→A) → Fun (^◡g ∪ ((A ∖ ran g) × {z})))
44		f1f 2781	. . . . . . . . . . . . . . . . 17 ⊢ (g:B–1-1→A → g:B–→A)
45		frn 2757	. . . . . . . . . . . . . . . . 17 ⊢ (g:B–→A → ran g ⊆ A)
46	44, 45	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (g:B–1-1→A → ran g ⊆ A)
47		ssundif 1764	. . . . . . . . . . . . . . . 16 ⊢ (ran g ⊆ A ↔ (ran g ∪ (A ∖ ran g)) = A)
48	46, 47	sylib 173	. . . . . . . . . . . . . . 15 ⊢ (g:B–1-1→A → (ran g ∪ (A ∖ ran g)) = A)
49		dmun 2536	. . . . . . . . . . . . . . . 16 ⊢ dom (^◡g ∪ ((A ∖ ran g) × {z})) = (dom ^◡g ∪ dom ((A ∖ ran g) × {z}))
50	32	uneq1i 1607	. . . . . . . . . . . . . . . . 17 ⊢ (ran g ∪ dom ((A ∖ ran g) × {z})) = (dom ^◡g ∪ dom ((A ∖ ran g) × {z}))
51	36	uneq2i 1608	. . . . . . . . . . . . . . . . 17 ⊢ (ran g ∪ dom ((A ∖ ran g) × {z})) = (ran g ∪ (A ∖ ran g))
52	50, 51	eqtr3 1121	. . . . . . . . . . . . . . . 16 ⊢ (dom ^◡g ∪ dom ((A ∖ ran g) × {z})) = (ran g ∪ (A ∖ ran g))
53	49, 52	eqtr 1119	. . . . . . . . . . . . . . 15 ⊢ dom (^◡g ∪ ((A ∖ ran g) × {z})) = (ran g ∪ (A ∖ ran g))
54	48, 53	syl5eq 1136	. . . . . . . . . . . . . 14 ⊢ (g:B–1-1→A → dom (^◡g ∪ ((A ∖ ran g) × {z})) = A)
55	54	adantl 305	. . . . . . . . . . . . 13 ⊢ ((z ∈ B ∧ g:B–1-1→A) → dom (^◡g ∪ ((A ∖ ran g) × {z})) = A)
56	43, 55	jca 236	. . . . . . . . . . . 12 ⊢ ((z ∈ B ∧ g:B–1-1→A) → (Fun (^◡g ∪ ((A ∖ ran g) × {z})) ∧ dom (^◡g ∪ ((A ∖ ran g) × {z})) = A))
57		df-fn 2433	. . . . . . . . . . . 12 ⊢ ((^◡g ∪ ((A ∖ ran g) × {z})) Fn A ↔ (Fun (^◡g ∪ ((A ∖ ran g) × {z})) ∧ dom (^◡g ∪ ((A ∖ ran g) × {z})) = A))
58	56, 57	sylibr 175	. . . . . . . . . . 11 ⊢ ((z ∈ B ∧ g:B–1-1→A) → (^◡g ∪ ((A ∖ ran g) × {z})) Fn A)
59		fdm 2756	. . . . . . . . . . . . . . . . 17 ⊢ (g:B–→A → dom g = B)
60	44, 59	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (g:B–1-1→A → dom g = B)
61		dfdm4 2525	. . . . . . . . . . . . . . . 16 ⊢ dom g = ran ^◡g
62	60, 61	syl5eqr 1138	. . . . . . . . . . . . . . 15 ⊢ (g:B–1-1→A → ran ^◡g = B)
63	62	uneq1d 1610	. . . . . . . . . . . . . 14 ⊢ (g:B–1-1→A → (ran ^◡g ∪ ran ((A ∖ ran g) × {z})) = (B ∪ ran ((A ∖ ran g) × {z})))
64	63	adantl 305	. . . . . . . . . . . . 13 ⊢ ((z ∈ B ∧ g:B–1-1→A) → (ran ^◡g ∪ ran ((A ∖ ran g) × {z})) = (B ∪ ran ((A ∖ ran g) × {z})))
65		0ss 1725	. . . . . . . . . . . . . . . . . 18 ⊢ ∅ ⊆ B
66		xpeq1 2440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((A ∖ ran g) = ∅ → ((A ∖ ran g) × {z}) = (∅ × {z}))
67		xp0r 2474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ × {z}) = ∅
68	66, 67	syl6eq 1140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((A ∖ ran g) = ∅ → ((A ∖ ran g) × {z}) = ∅)
69	68	rneqd 2557	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((A ∖ ran g) = ∅ → ran ((A ∖ ran g) × {z}) = ran ∅)
70		rn0 2567	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran ∅ = ∅
71	69, 70	syl6eq 1140	. . . . . . . . . . . . . . . . . . 19 ⊢ ((A ∖ ran g) = ∅ → ran ((A ∖ ran g) × {z}) = ∅)
72	71	sseq1d 1527	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∖ ran g) = ∅ → (ran ((A ∖ ran g) × {z}) ⊆ B ↔ ∅ ⊆ B))
73	65, 72	mpbiri 169	. . . . . . . . . . . . . . . . 17 ⊢ ((A ∖ ran g) = ∅ → ran ((A ∖ ran g) × {z}) ⊆ B)
74	73	a1d 14	. . . . . . . . . . . . . . . 16 ⊢ ((A ∖ ran g) = ∅ → (z ∈ B → ran ((A ∖ ran g) × {z}) ⊆ B))
75		rnxp 2657	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (A ∖ ran g) = ∅ → ran ((A ∖ ran g) × {z}) = {z})
76	75	adantr 306	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ (A ∖ ran g) = ∅ ∧ z ∈ B) → ran ((A ∖ ran g) × {z}) = {z})
77		snssi 1851	. . . . . . . . . . . . . . . . . . 19 ⊢ (z ∈ B → {z} ⊆ B)
78	77	adantl 305	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ (A ∖ ran g) = ∅ ∧ z ∈ B) → {z} ⊆ B)
79	76, 78	eqsstrd 1534	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ (A ∖ ran g) = ∅ ∧ z ∈ B) → ran ((A ∖ ran g) × {z}) ⊆ B)
80	79	exp 291	. . . . . . . . . . . . . . . 16 ⊢ (¬ (A ∖ ran g) = ∅ → (z ∈ B → ran ((A ∖ ran g) × {z}) ⊆ B))
81	74, 80	pm2.61i 110	. . . . . . . . . . . . . . 15 ⊢ (z ∈ B → ran ((A ∖ ran g) × {z}) ⊆ B)
82		ssequn2 1631	. . . . . . . . . . . . . . 15 ⊢ (ran ((A ∖ ran g) × {z}) ⊆ B ↔ (B ∪ ran ((A ∖ ran g) × {z})) = B)
83	81, 82	sylib 173	. . . . . . . . . . . . . 14 ⊢ (z ∈ B → (B ∪ ran ((A ∖ ran g) × {z})) = B)
84	83	adantr 306	. . . . . . . . . . . . 13 ⊢ ((z ∈ B ∧ g:B–1-1→A) → (B ∪ ran ((A ∖ ran g) × {z})) = B)
85	64, 84	eqtrd 1128	. . . . . . . . . . . 12 ⊢ ((z ∈ B ∧ g:B–1-1→A) → (ran ^◡g ∪ ran ((A ∖ ran g) × {z})) = B)
86		rnun 2644	. . . . . . . . . . . 12 ⊢ ran (^◡g ∪ ((A ∖ ran g) × {z})) = (ran ^◡g ∪ ran ((A ∖ ran g) × {z}))
87	85, 86	syl5eq 1136	. . . . . . . . . . 11 ⊢ ((z ∈ B ∧ g:B–1-1→A) → ran (^◡g ∪ ((A ∖ ran g) × {z})) = B)
88	58, 87	jca 236	. . . . . . . . . 10 ⊢ ((z ∈ B ∧ g:B–1-1→A) → ((^◡g ∪ ((A ∖ ran g) × {z})) Fn A ∧ ran (^◡g ∪ ((A ∖ ran g) × {z})) = B))
89		df-fo 2436	. . . . . . . . . 10 ⊢ ((^◡g ∪ ((A ∖ ran g) × {z})):A–onto→B ↔ ((^◡g ∪ ((A ∖ ran g) × {z})) Fn A ∧ ran (^◡g ∪ ((A ∖ ran g) × {z})) = B))
90	88, 89	sylibr 175	. . . . . . . . 9 ⊢ ((z ∈ B ∧ g:B–1-1→A) → (^◡g ∪ ((A ∖ ran g) × {z})):A–onto→B)
91		visset 1350	. . . . . . . . . . . 12 ⊢ g ∈ V
92	91	cnvex 2670	. . . . . . . . . . 11 ⊢ ^◡g ∈ V
93		difexg 1703	. . . . . . . . . . . . 13 ⊢ (A ∈ V → (A ∖ ran g) ∈ V)
94	15, 93	ax-mp 6	. . . . . . . . . . . 12 ⊢ (A ∖ ran g) ∈ V
95		snex 1859	. . . . . . . . . . . 12 ⊢ {z} ∈ V
96	94, 95	xpex 2488	. . . . . . . . . . 11 ⊢ ((A ∖ ran g) × {z}) ∈ V
97	92, 96	unex 1949	. . . . . . . . . 10 ⊢ (^◡g ∪ ((A ∖ ran g) × {z})) ∈ V
98		foeq1 2784	. . . . . . . . . 10 ⊢ (f = (^◡g ∪ ((A ∖ ran g) × {z})) → (f:A–onto→B ↔ (^◡g ∪ ((A ∖ ran g) × {z})):A–onto→B))
99	97, 98	cla4ev 1401	. . . . . . . . 9 ⊢ ((^◡g ∪ ((A ∖ ran g) × {z})):A–onto→B → ∃f f:A–onto→B)
100	90, 99	syl 12	. . . . . . . 8 ⊢ ((z ∈ B ∧ g:B–1-1→A) → ∃f f:A–onto→B)
101	100	exp 291	. . . . . . 7 ⊢ (z ∈ B → (g:B–1-1→A → ∃f f:A–onto→B))
102	101	19.23adv 954	. . . . . 6 ⊢ (z ∈ B → (∃g g:B–1-1→A → ∃f f:A–onto→B))
103	102	19.23aiv 952	. . . . 5 ⊢ (∃z z ∈ B → (∃g g:B–1-1→A → ∃f f:A–onto→B))
104	103	imp 277	. . . 4 ⊢ ((∃z z ∈ B ∧ ∃g g:B–1-1→A) → ∃f f:A–onto→B)
105		n0 1714	. . . . 5 ⊢ (¬ B = ∅ ↔ ∃z z ∈ B)
106	13, 105	bitr 151	. . . 4 ⊢ (∅ ≺ B ↔ ∃z z ∈ B)
107	15	brdom 3283	. . . 4 ⊢ (B ≼ A ↔ ∃g g:B–1-1→A)
108	104, 106, 107	syl2anb 350	. . 3 ⊢ ((∅ ≺ B ∧ B ≼ A) → ∃f f:A–onto→B)
109	24, 108	jca 236	. 2 ⊢ ((∅ ≺ B ∧ B ≼ A) → (¬ A = ∅ ∧ ∃f f:A–onto→B))
110	20, 109	impbi 139	1 ⊢ ((¬ A = ∅ ∧ ∃f f:A–onto→B) ↔ (∅ ≺ B ∧ B ≼ A))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∃wex 678 = wceq 1091 ∈ wcel 1092 Vcvv 1348 ∖ cdif 1484 ∪ cun 1485 ∩ cin 1486 ⊆ wss 1487 ∅c0 1707 {csn 1808 class class class wbr 2054 × cxp 2408 ^◡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 ≺ csdm 3273

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-er 3200 df-en 3274 df-dom 3275 df-sdom 3276

metamath.org