Theorem fodomr 9153

Description: There exists a mapping from a set onto any (nonempty) set that it dominates. (Contributed by NM, 23-Mar-2006.)

Assertion

Ref	Expression
fodomr	⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)

Distinct variable groups:   𝐴,𝑓   𝐵,𝑓

Proof of Theorem fodomr

Dummy variables 𝑔 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldom 8970	. . . 4 ⊢ Rel ≼
2	1	brrelex2i 5735	. . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐴 ∈ V)
3	2	adantl 480	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V)
4	1	brrelex1i 5734	. . . 4 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V)
5		0sdomg 9129	. . . . 5 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅))
6		n0 4346	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐵)
7	5, 6	bitrdi 286	. . . 4 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
8	4, 7	syl 17	. . 3 ⊢ (𝐵 ≼ 𝐴 → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
9	8	biimpac 477	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑧 𝑧 ∈ 𝐵)
10		brdomi 8979	. . 3 ⊢ (𝐵 ≼ 𝐴 → ∃𝑔 𝑔:𝐵–1-1→𝐴)
11	10	adantl 480	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑔 𝑔:𝐵–1-1→𝐴)
12		difexg 5330	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (𝐴 ∖ ran 𝑔) ∈ V)
13		vsnex 5431	. . . . . . . . . 10 ⊢ {𝑧} ∈ V
14		xpexg 7753	. . . . . . . . . 10 ⊢ (((𝐴 ∖ ran 𝑔) ∈ V ∧ {𝑧} ∈ V) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
15	12, 13, 14	sylancl 584	. . . . . . . . 9 ⊢ (𝐴 ∈ V → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
16		vex 3465	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
17	16	cnvex 7933	. . . . . . . . 9 ⊢ ◡𝑔 ∈ V
18	15, 17	jctil 518	. . . . . . . 8 ⊢ (𝐴 ∈ V → (◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V))
19		unexb 7751	. . . . . . . 8 ⊢ ((◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V) ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
20	18, 19	sylib 217	. . . . . . 7 ⊢ (𝐴 ∈ V → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
21		df-f1 6554	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔))
22	21	simprbi 495	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun ◡𝑔)
23		vex 3465	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
24	23	fconst 6783	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧}
25		ffun 6726	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝐴 ∖ ran 𝑔) × {𝑧}))
26	24, 25	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})
27	22, 26	jctir 519	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})))
28		df-rn 5689	. . . . . . . . . . . . . 14 ⊢ ran 𝑔 = dom ◡𝑔
29	28	eqcomi 2734	. . . . . . . . . . . . 13 ⊢ dom ◡𝑔 = ran 𝑔
30	23	snnz 4782	. . . . . . . . . . . . . 14 ⊢ {𝑧} ≠ ∅
31		dmxp 5931	. . . . . . . . . . . . . 14 ⊢ ({𝑧} ≠ ∅ → dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)
33	29, 32	ineq12i 4208	. . . . . . . . . . . 12 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔))
34		disjdif 4473	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅
35	33, 34	eqtri 2753	. . . . . . . . . . 11 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅
36		funun 6600	. . . . . . . . . . 11 ⊢ (((Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
37	27, 35, 36	sylancl 584	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
38	37	adantl 480	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
39		dmun 5913	. . . . . . . . . . . 12 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
40	28	uneq1i 4156	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
41	32	uneq2i 4157	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
42	39, 40, 41	3eqtr2i 2759	. . . . . . . . . . 11 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
43		f1f 6793	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔:𝐵⟶𝐴)
44	43	frnd 6731	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → ran 𝑔 ⊆ 𝐴)
45		undif 4483	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ⊆ 𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
46	44, 45	sylib 217	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
47	42, 46	eqtrid 2777	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
48	47	adantl 480	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
49		df-fn 6552	. . . . . . . . 9 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴))
50	38, 48, 49	sylanbrc 581	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴)
51		rnun 6152	. . . . . . . . 9 ⊢ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))
52		dfdm4 5898	. . . . . . . . . . . 12 ⊢ dom 𝑔 = ran ◡𝑔
53		f1dm 6797	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → dom 𝑔 = 𝐵)
54	52, 53	eqtr3id 2779	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → ran ◡𝑔 = 𝐵)
55	54	uneq1d 4159	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})))
56		xpeq1 5692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧}))
57		0xp 5776	. . . . . . . . . . . . . . . . 17 ⊢ (∅ × {𝑧}) = ∅
58	56, 57	eqtrdi 2781	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
59	58	rneqd 5940	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅)
60		rn0 5928	. . . . . . . . . . . . . . 15 ⊢ ran ∅ = ∅
61	59, 60	eqtrdi 2781	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
62		0ss 4398	. . . . . . . . . . . . . 14 ⊢ ∅ ⊆ 𝐵
63	61, 62	eqsstrdi 4031	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
64	63	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
65		rnxp 6176	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
66	65	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
67		snssi 4813	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → {𝑧} ⊆ 𝐵)
68	67	adantl 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → {𝑧} ⊆ 𝐵)
69	66, 68	eqsstrd 4015	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
70	69	ex 411	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
71	64, 70	pm2.61ine 3014	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
72		ssequn2 4181	. . . . . . . . . . 11 ⊢ (ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
73	71, 72	sylib 217	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
74	55, 73	sylan9eqr 2787	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
75	51, 74	eqtrid 2777	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
76		df-fo 6555	. . . . . . . 8 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 ↔ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵))
77	50, 75, 76	sylanbrc 581	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵)
78		foeq1 6806	. . . . . . . 8 ⊢ (𝑓 = (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝐴–onto→𝐵 ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵))
79	78	spcegv 3581	. . . . . . 7 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V → ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))
80	20, 77, 79	syl2im 40	. . . . . 6 ⊢ (𝐴 ∈ V → ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵))
81	80	expdimp 451	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝐵) → (𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵))
82	81	exlimdv 1928	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝐵) → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵))
83	82	ex 411	. . 3 ⊢ (𝐴 ∈ V → (𝑧 ∈ 𝐵 → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵)))
84	83	exlimdv 1928	. 2 ⊢ (𝐴 ∈ V → (∃𝑧 𝑧 ∈ 𝐵 → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵)))
85	3, 9, 11, 84	syl3c 66	1 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533  ∃wex 1773   ∈ wcel 2098   ≠ wne 2929  Vcvv 3461   ∖ cdif 3941   ∪ cun 3942   ∩ cin 3943   ⊆ wss 3944  ∅c0 4322  {csn 4630   class class class wbr 5149   × cxp 5676  ^◡ccnv 5677  dom cdm 5678  ran crn 5679  Fun wfun 6543   Fn wfn 6544  ⟶wf 6545  –1-1→wf1 6546  –onto→wfo 6547   ≼ cdom 8962   ≺ csdm 8963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-en 8965  df-dom 8966  df-sdom 8967

This theorem is referenced by:  pwdom  9154  fodomfib  9352  domwdom  9599  iunfictbso  10139  fodomb  10551  brdom3  10553  konigthlem  10593  1stcfb  23393  ovoliunnul  25480  sigapildsys  33912  carsgclctunlem3  34071  ovoliunnfl  37266  voliunnfl  37268  volsupnfl  37269  nnfoctb  44553  caragenunicl  46050