Theorem fodomr 9123

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 8955	. . . 4 ⊢ Rel ≼
2	1	brrelex2i 5720	. . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐴 ∈ V)
3	2	adantl 487	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V)
4	1	brrelex1i 5719	. . . 4 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V)
5		0sdomg 9101	. . . . 5 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅))
6		n0 4307	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐵)
7	5, 6	bitrdi 290	. . . 4 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
8	4, 7	syl 18	. . 3 ⊢ (𝐵 ≼ 𝐴 → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
9	8	biimpac 484	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑧 𝑧 ∈ 𝐵)
10		brdomi 8962	. . 3 ⊢ (𝐵 ≼ 𝐴 → ∃𝑔 𝑔:𝐵–1-1→𝐴)
11	10	adantl 487	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑔 𝑔:𝐵–1-1→𝐴)
12		difexg 5302	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (𝐴 ∖ ran 𝑔) ∈ V)
13		vsnex 5408	. . . . . . . . . 10 ⊢ {𝑧} ∈ V
14		xpexg 7755	. . . . . . . . . 10 ⊢ (((𝐴 ∖ ran 𝑔) ∈ V ∧ {𝑧} ∈ V) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
15	12, 13, 14	sylancl 598	. . . . . . . . 9 ⊢ (𝐴 ∈ V → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
16		vex 3461	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
17	16	cnvex 7928	. . . . . . . . 9 ⊢ ◡𝑔 ∈ V
18	15, 17	jctil 529	. . . . . . . 8 ⊢ (𝐴 ∈ V → (◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V))
19		unexb 7754	. . . . . . . 8 ⊢ ((◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V) ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
20	18, 19	sylib 221	. . . . . . 7 ⊢ (𝐴 ∈ V → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
21		df-f1 6545	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔))
22	21	simprbi 503	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun ◡𝑔)
23		vex 3461	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
24	23	fconst 6768	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧}
25		ffun 6712	. . . . . . . . . . . . 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 5674	. . . . . . . . . . . . . 14 ⊢ ran 𝑔 = dom ◡𝑔
29	28	eqcomi 2774	. . . . . . . . . . . . 13 ⊢ dom ◡𝑔 = ran 𝑔
30	23	snnz 4744	. . . . . . . . . . . . . 14 ⊢ {𝑧} ≠ ∅
31		dmxp 5921	. . . . . . . . . . . . . 14 ⊢ ({𝑧} ≠ ∅ → dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)
33	29, 32	ineq12i 4171	. . . . . . . . . . . 12 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔))
34		disjdif 4433	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅
35	33, 34	eqtri 2788	. . . . . . . . . . 11 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅
36		funun 6586	. . . . . . . . . . 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 5902	. . . . . . . . . . . 12 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
40	28	uneq1i 4118	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
41	32	uneq2i 4119	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
42	39, 40, 41	3eqtr2i 2794	. . . . . . . . . . 11 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
43		f1f 6778	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔:𝐵⟶𝐴)
44	43	frnd 6718	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → ran 𝑔 ⊆ 𝐴)
45		undif 4445	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ⊆ 𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
46	44, 45	sylib 221	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
47	42, 46	eqtrid 2812	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
48	47	adantl 487	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
49		df-fn 6543	. . . . . . . . 9 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴))
50	38, 48, 49	sylanbrc 595	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴)
51		rnun 6144	. . . . . . . . 9 ⊢ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))
52		dfdm4 5887	. . . . . . . . . . . 12 ⊢ dom 𝑔 = ran ◡𝑔
53		f1dm 6784	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → dom 𝑔 = 𝐵)
54	52, 53	eqtr3id 2814	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → ran ◡𝑔 = 𝐵)
55	54	uneq1d 4121	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})))
56		xpeq1 5677	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧}))
57		0xp 5762	. . . . . . . . . . . . . . . . 17 ⊢ (∅ × {𝑧}) = ∅
58	56, 57	eqtrdi 2816	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
59	58	rneqd 5930	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅)
60		rn0 5918	. . . . . . . . . . . . . . 15 ⊢ ran ∅ = ∅
61	59, 60	eqtrdi 2816	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
62		0ss 4357	. . . . . . . . . . . . . 14 ⊢ ∅ ⊆ 𝐵
63	61, 62	eqsstrdi 3982	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
64	63	a1d 26	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
65		rnxp 6170	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
66	65	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
67		snssi 4753	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → {𝑧} ⊆ 𝐵)
68	67	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → {𝑧} ⊆ 𝐵)
69	66, 68	eqsstrd 3972	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
70	69	ex 418	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
71	64, 70	pm2.61ine 3043	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
72		ssequn2 4142	. . . . . . . . . . 11 ⊢ (ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
73	71, 72	sylib 221	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
74	55, 73	sylan9eqr 2822	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
75	51, 74	eqtrid 2812	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
76		df-fo 6546	. . . . . . . 8 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 ↔ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵))
77	50, 75, 76	sylanbrc 595	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵)
78		foeq1 6792	. . . . . . . 8 ⊢ (𝑓 = (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝐴–onto→𝐵 ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵))
79	78	spcegv 3558	. . . . . . 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 2146   ≠ wne 2960  Vcvv 3457   ∖ cdif 3903   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  {csn 4591   class class class wbr 5111   × cxp 5661  ^◡ccnv 5662  dom cdm 5663  ran crn 5664  Fun wfun 6534   Fn wfn 6535  ⟶wf 6536  –1-1→wf1 6537  –onto→wfo 6538   ≼ cdom 8947   ≺ csdm 8948

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-en 8950  df-dom 8951  df-sdom 8952

This theorem is used by:  pwdom  9124  domwdom  9543  iunfictbso  10114  fodomb  10525  brdom3  10527  konigthlem  10568  1stcfb  23652  ovoliunnul  25717  sigapildsys  34617  carsgclctunlem3  34775  ovoliunnfl  38370  voliunnfl  38372  volsupnfl  38373  modelaxreplem1  45745  nnfoctb  45826  caragenunicl  47296