Theorem fodomr 9140

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 8972	. . . 4 ⊢ Rel ≼
2	1	brrelex2i 5708	. . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐴 ∈ V)
3	2	adantl 487	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V)
4	1	brrelex1i 5707	. . . 4 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V)
5		0sdomg 9118	. . . . 5 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅))
6		n0 4300	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐵)
7	5, 6	bitrdi 290	. . . 4 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
8	4, 7	syl 18	. . 3 ⊢ (𝐵 ≼ 𝐴 → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
9	8	biimpac 484	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑧 𝑧 ∈ 𝐵)
10		brdomi 8979	. . 3 ⊢ (𝐵 ≼ 𝐴 → ∃𝑔 𝑔:𝐵–1-1→𝐴)
11	10	adantl 487	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑔 𝑔:𝐵–1-1→𝐴)
12		difexg 5291	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (𝐴 ∖ ran 𝑔) ∈ V)
13		vsnex 5393	. . . . . . . . . 10 ⊢ {𝑧} ∈ V
14		xpexg 7762	. . . . . . . . . 10 ⊢ (((𝐴 ∖ ran 𝑔) ∈ V ∧ {𝑧} ∈ V) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
15	12, 13, 14	sylancl 598	. . . . . . . . 9 ⊢ (𝐴 ∈ V → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
16		vex 3455	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
17	16	cnvex 7935	. . . . . . . . 9 ⊢ ◡𝑔 ∈ V
18	15, 17	jctil 529	. . . . . . . 8 ⊢ (𝐴 ∈ V → (◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V))
19		unexb 7761	. . . . . . . 8 ⊢ ((◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V) ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
20	18, 19	sylib 221	. . . . . . 7 ⊢ (𝐴 ∈ V → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
21		df-f1 6542	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔))
22	21	simprbi 503	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun ◡𝑔)
23		vex 3455	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
24	23	fconst 6766	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧}
25		ffun 6710	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝐴 ∖ ran 𝑔) × {𝑧}))
26	24, 25	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})
27	22, 26	jctir 530	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})))
28		df-rn 5662	. . . . . . . . . . . . . 14 ⊢ ran 𝑔 = dom ◡𝑔
29	28	eqcomi 2770	. . . . . . . . . . . . 13 ⊢ dom ◡𝑔 = ran 𝑔
30	23	snnz 4737	. . . . . . . . . . . . . 14 ⊢ {𝑧} ≠ ∅
31		dmxp 5911	. . . . . . . . . . . . . 14 ⊢ ({𝑧} ≠ ∅ → dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)
33	29, 32	ineq12i 4164	. . . . . . . . . . . 12 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔))
34		disjdif 4426	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅
35	33, 34	eqtri 2784	. . . . . . . . . . 11 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅
36		funun 6584	. . . . . . . . . . 11 ⊢ (((Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
37	27, 35, 36	sylancl 598	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
38	37	adantl 487	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
39		dmun 5892	. . . . . . . . . . . 12 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
40	28	uneq1i 4111	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
41	32	uneq2i 4112	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
42	39, 40, 41	3eqtr2i 2790	. . . . . . . . . . 11 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
43		f1f 6776	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔:𝐵⟶𝐴)
44	43	frnd 6716	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → ran 𝑔 ⊆ 𝐴)
45		undif 4438	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ⊆ 𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
46	44, 45	sylib 221	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
47	42, 46	eqtrid 2808	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
48	47	adantl 487	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
49		df-fn 6540	. . . . . . . . 9 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴))
50	38, 48, 49	sylanbrc 595	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴)
51		rnun 6136	. . . . . . . . 9 ⊢ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))
52		dfdm4 5877	. . . . . . . . . . . 12 ⊢ dom 𝑔 = ran ◡𝑔
53		f1dm 6782	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → dom 𝑔 = 𝐵)
54	52, 53	eqtr3id 2810	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → ran ◡𝑔 = 𝐵)
55	54	uneq1d 4114	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})))
56		xpeq1 5665	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧}))
57		0xp 5750	. . . . . . . . . . . . . . . . 17 ⊢ (∅ × {𝑧}) = ∅
58	56, 57	eqtrdi 2812	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
59	58	rneqd 5920	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅)
60		rn0 5908	. . . . . . . . . . . . . . 15 ⊢ ran ∅ = ∅
61	59, 60	eqtrdi 2812	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
62		0ss 4350	. . . . . . . . . . . . . 14 ⊢ ∅ ⊆ 𝐵
63	61, 62	eqsstrdi 3975	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
64	63	a1d 26	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
65		rnxp 6162	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
66	65	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
67		snssi 4746	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → {𝑧} ⊆ 𝐵)
68	67	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → {𝑧} ⊆ 𝐵)
69	66, 68	eqsstrd 3965	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
70	69	ex 418	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
71	64, 70	pm2.61ine 3039	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
72		ssequn2 4135	. . . . . . . . . . 11 ⊢ (ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
73	71, 72	sylib 221	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
74	55, 73	sylan9eqr 2818	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
75	51, 74	eqtrid 2808	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
76		df-fo 6543	. . . . . . . 8 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 ↔ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵))
77	50, 75, 76	sylanbrc 595	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵)
78		foeq1 6790	. . . . . . . 8 ⊢ (𝑓 = (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝐴–onto→𝐵 ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵))
79	78	spcegv 3552	. . . . . . 7 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V → ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 → ∃𝑓 𝑓:𝐴–onto→𝐵))
80	20, 77, 79	syl2im 41	. . . . . 6 ⊢ (𝐴 ∈ V → ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵))
81	80	expdimp 458	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝐵) → (𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵))
82	81	exlimdv 1966	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝐵) → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵))
83	82	ex 418	. . 3 ⊢ (𝐴 ∈ V → (𝑧 ∈ 𝐵 → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵)))
84	83	exlimdv 1966	. 2 ⊢ (𝐴 ∈ V → (∃𝑧 𝑧 ∈ 𝐵 → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵)))
85	3, 9, 11, 84	syl3c 67	1 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  {csn 4584   class class class wbr 5103   × cxp 5649  ^◡ccnv 5650  dom cdm 5651  ran crn 5652  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  –1-1→wf1 6534  –onto→wfo 6535   ≼ cdom 8964   ≺ csdm 8965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-en 8967  df-dom 8968  df-sdom 8969

This theorem is used by:  pwdom  9141  domwdom  9561  iunfictbso  10186  fodomb  10598  brdom3  10600  konigthlem  10646  1stcfb  23756  ovoliunnul  25821  sigapildsys  34788  carsgclctunlem3  34945  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  modelaxreplem1  45946  nnfoctb  46034  caragenunicl  47503