Theorem fodomr 9168

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 8991	. . . 4 ⊢ Rel ≼
2	1	brrelex2i 5742	. . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐴 ∈ V)
3	2	adantl 481	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V)
4	1	brrelex1i 5741	. . . 4 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V)
5		0sdomg 9144	. . . . 5 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅))
6		n0 4353	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐵)
7	5, 6	bitrdi 287	. . . 4 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
8	4, 7	syl 17	. . 3 ⊢ (𝐵 ≼ 𝐴 → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
9	8	biimpac 478	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑧 𝑧 ∈ 𝐵)
10		brdomi 8999	. . 3 ⊢ (𝐵 ≼ 𝐴 → ∃𝑔 𝑔:𝐵–1-1→𝐴)
11	10	adantl 481	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑔 𝑔:𝐵–1-1→𝐴)
12		difexg 5329	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (𝐴 ∖ ran 𝑔) ∈ V)
13		vsnex 5434	. . . . . . . . . 10 ⊢ {𝑧} ∈ V
14		xpexg 7770	. . . . . . . . . 10 ⊢ (((𝐴 ∖ ran 𝑔) ∈ V ∧ {𝑧} ∈ V) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
15	12, 13, 14	sylancl 586	. . . . . . . . 9 ⊢ (𝐴 ∈ V → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
16		vex 3484	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
17	16	cnvex 7947	. . . . . . . . 9 ⊢ ◡𝑔 ∈ V
18	15, 17	jctil 519	. . . . . . . 8 ⊢ (𝐴 ∈ V → (◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V))
19		unexb 7767	. . . . . . . 8 ⊢ ((◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V) ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
20	18, 19	sylib 218	. . . . . . 7 ⊢ (𝐴 ∈ V → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
21		df-f1 6566	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔))
22	21	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun ◡𝑔)
23		vex 3484	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
24	23	fconst 6794	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧}
25		ffun 6739	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝐴 ∖ ran 𝑔) × {𝑧}))
26	24, 25	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})
27	22, 26	jctir 520	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})))
28		df-rn 5696	. . . . . . . . . . . . . 14 ⊢ ran 𝑔 = dom ◡𝑔
29	28	eqcomi 2746	. . . . . . . . . . . . 13 ⊢ dom ◡𝑔 = ran 𝑔
30	23	snnz 4776	. . . . . . . . . . . . . 14 ⊢ {𝑧} ≠ ∅
31		dmxp 5939	. . . . . . . . . . . . . 14 ⊢ ({𝑧} ≠ ∅ → dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)
33	29, 32	ineq12i 4218	. . . . . . . . . . . 12 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔))
34		disjdif 4472	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅
35	33, 34	eqtri 2765	. . . . . . . . . . 11 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅
36		funun 6612	. . . . . . . . . . 11 ⊢ (((Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
37	27, 35, 36	sylancl 586	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
38	37	adantl 481	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
39		dmun 5921	. . . . . . . . . . . 12 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
40	28	uneq1i 4164	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
41	32	uneq2i 4165	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
42	39, 40, 41	3eqtr2i 2771	. . . . . . . . . . 11 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
43		f1f 6804	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔:𝐵⟶𝐴)
44	43	frnd 6744	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → ran 𝑔 ⊆ 𝐴)
45		undif 4482	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ⊆ 𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
46	44, 45	sylib 218	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
47	42, 46	eqtrid 2789	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
48	47	adantl 481	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
49		df-fn 6564	. . . . . . . . 9 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴))
50	38, 48, 49	sylanbrc 583	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴)
51		rnun 6165	. . . . . . . . 9 ⊢ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))
52		dfdm4 5906	. . . . . . . . . . . 12 ⊢ dom 𝑔 = ran ◡𝑔
53		f1dm 6808	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → dom 𝑔 = 𝐵)
54	52, 53	eqtr3id 2791	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → ran ◡𝑔 = 𝐵)
55	54	uneq1d 4167	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})))
56		xpeq1 5699	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧}))
57		0xp 5784	. . . . . . . . . . . . . . . . 17 ⊢ (∅ × {𝑧}) = ∅
58	56, 57	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
59	58	rneqd 5949	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅)
60		rn0 5936	. . . . . . . . . . . . . . 15 ⊢ ran ∅ = ∅
61	59, 60	eqtrdi 2793	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
62		0ss 4400	. . . . . . . . . . . . . 14 ⊢ ∅ ⊆ 𝐵
63	61, 62	eqsstrdi 4028	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
64	63	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
65		rnxp 6190	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
66	65	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
67		snssi 4808	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → {𝑧} ⊆ 𝐵)
68	67	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → {𝑧} ⊆ 𝐵)
69	66, 68	eqsstrd 4018	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
70	69	ex 412	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
71	64, 70	pm2.61ine 3025	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
72		ssequn2 4189	. . . . . . . . . . 11 ⊢ (ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
73	71, 72	sylib 218	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
74	55, 73	sylan9eqr 2799	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
75	51, 74	eqtrid 2789	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
76		df-fo 6567	. . . . . . . 8 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 ↔ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵))
77	50, 75, 76	sylanbrc 583	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵)
78		foeq1 6816	. . . . . . . 8 ⊢ (𝑓 = (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝐴–onto→𝐵 ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵))
79	78	spcegv 3597	. . . . . . 7 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V → ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))
80	20, 77, 79	syl2im 40	. . . . . 6 ⊢ (𝐴 ∈ V → ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵))
81	80	expdimp 452	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝐵) → (𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵))
82	81	exlimdv 1933	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝐵) → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵))
83	82	ex 412	. . 3 ⊢ (𝐴 ∈ V → (𝑧 ∈ 𝐵 → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵)))
84	83	exlimdv 1933	. 2 ⊢ (𝐴 ∈ V → (∃𝑧 𝑧 ∈ 𝐵 → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵)))
85	3, 9, 11, 84	syl3c 66	1 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  {csn 4626   class class class wbr 5143   × cxp 5683  ^◡ccnv 5684  dom cdm 5685  ran crn 5686  Fun wfun 6555   Fn wfn 6556  ⟶wf 6557  –1-1→wf1 6558  –onto→wfo 6559   ≼ cdom 8983   ≺ csdm 8984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-en 8986  df-dom 8987  df-sdom 8988

This theorem is referenced by:  pwdom  9169  fodomfibOLD  9371  domwdom  9614  iunfictbso  10154  fodomb  10566  brdom3  10568  konigthlem  10608  1stcfb  23453  ovoliunnul  25542  sigapildsys  34163  carsgclctunlem3  34322  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  modelaxreplem1  44995  nnfoctb  45053  caragenunicl  46539