Theorem fodomr 8668

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 8515	. . . 4 ⊢ Rel ≼
2	1	brrelex2i 5609	. . 3 ⊢ (𝐵 ≼ 𝐴 → 𝐴 ∈ V)
3	2	adantl 484	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ∈ V)
4	1	brrelex1i 5608	. . . 4 ⊢ (𝐵 ≼ 𝐴 → 𝐵 ∈ V)
5		0sdomg 8646	. . . . 5 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ 𝐵 ≠ ∅))
6		n0 4310	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐵)
7	5, 6	syl6bb 289	. . . 4 ⊢ (𝐵 ∈ V → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
8	4, 7	syl 17	. . 3 ⊢ (𝐵 ≼ 𝐴 → (∅ ≺ 𝐵 ↔ ∃𝑧 𝑧 ∈ 𝐵))
9	8	biimpac 481	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑧 𝑧 ∈ 𝐵)
10		brdomi 8520	. . 3 ⊢ (𝐵 ≼ 𝐴 → ∃𝑔 𝑔:𝐵–1-1→𝐴)
11	10	adantl 484	. 2 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑔 𝑔:𝐵–1-1→𝐴)
12		difexg 5231	. . . . . . . . . 10 ⊢ (𝐴 ∈ V → (𝐴 ∖ ran 𝑔) ∈ V)
13		snex 5332	. . . . . . . . . 10 ⊢ {𝑧} ∈ V
14		xpexg 7473	. . . . . . . . . 10 ⊢ (((𝐴 ∖ ran 𝑔) ∈ V ∧ {𝑧} ∈ V) → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
15	12, 13, 14	sylancl 588	. . . . . . . . 9 ⊢ (𝐴 ∈ V → ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V)
16		vex 3497	. . . . . . . . . 10 ⊢ 𝑔 ∈ V
17	16	cnvex 7630	. . . . . . . . 9 ⊢ ◡𝑔 ∈ V
18	15, 17	jctil 522	. . . . . . . 8 ⊢ (𝐴 ∈ V → (◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V))
19		unexb 7471	. . . . . . . 8 ⊢ ((◡𝑔 ∈ V ∧ ((𝐴 ∖ ran 𝑔) × {𝑧}) ∈ V) ↔ (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
20	18, 19	sylib 220	. . . . . . 7 ⊢ (𝐴 ∈ V → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∈ V)
21		df-f1 6360	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 ↔ (𝑔:𝐵⟶𝐴 ∧ Fun ◡𝑔))
22	21	simprbi 499	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun ◡𝑔)
23		vex 3497	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
24	23	fconst 6565	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧}
25		ffun 6517	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) × {𝑧}):(𝐴 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝐴 ∖ ran 𝑔) × {𝑧}))
26	24, 25	ax-mp 5	. . . . . . . . . . . 12 ⊢ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})
27	22, 26	jctir 523	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})))
28		df-rn 5566	. . . . . . . . . . . . . 14 ⊢ ran 𝑔 = dom ◡𝑔
29	28	eqcomi 2830	. . . . . . . . . . . . 13 ⊢ dom ◡𝑔 = ran 𝑔
30	23	snnz 4711	. . . . . . . . . . . . . 14 ⊢ {𝑧} ≠ ∅
31		dmxp 5799	. . . . . . . . . . . . . 14 ⊢ ({𝑧} ≠ ∅ → dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔))
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13 ⊢ dom ((𝐴 ∖ ran 𝑔) × {𝑧}) = (𝐴 ∖ ran 𝑔)
33	29, 32	ineq12i 4187	. . . . . . . . . . . 12 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔))
34		disjdif 4421	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∩ (𝐴 ∖ ran 𝑔)) = ∅
35	33, 34	eqtri 2844	. . . . . . . . . . 11 ⊢ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅
36		funun 6400	. . . . . . . . . . 11 ⊢ (((Fun ◡𝑔 ∧ Fun ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ (dom ◡𝑔 ∩ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
37	27, 35, 36	sylancl 588	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
38	37	adantl 484	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})))
39		dmun 5779	. . . . . . . . . . . 12 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
40	28	uneq1i 4135	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧}))
41	32	uneq2i 4136	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ∪ dom ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
42	39, 40, 41	3eqtr2i 2850	. . . . . . . . . . 11 ⊢ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔))
43		f1f 6575	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔:𝐵⟶𝐴)
44	43	frnd 6521	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → ran 𝑔 ⊆ 𝐴)
45		undif 4430	. . . . . . . . . . . 12 ⊢ (ran 𝑔 ⊆ 𝐴 ↔ (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
46	44, 45	sylib 220	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran 𝑔 ∪ (𝐴 ∖ ran 𝑔)) = 𝐴)
47	42, 46	syl5eq 2868	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
48	47	adantl 484	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴)
49		df-fn 6358	. . . . . . . . 9 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ↔ (Fun (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) ∧ dom (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐴))
50	38, 48, 49	sylanbrc 585	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴)
51		rnun 6004	. . . . . . . . 9 ⊢ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧}))
52		dfdm4 5764	. . . . . . . . . . . 12 ⊢ dom 𝑔 = ran ◡𝑔
53		f1dm 6579	. . . . . . . . . . . 12 ⊢ (𝑔:𝐵–1-1→𝐴 → dom 𝑔 = 𝐵)
54	52, 53	syl5eqr 2870	. . . . . . . . . . 11 ⊢ (𝑔:𝐵–1-1→𝐴 → ran ◡𝑔 = 𝐵)
55	54	uneq1d 4138	. . . . . . . . . 10 ⊢ (𝑔:𝐵–1-1→𝐴 → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})))
56		xpeq1 5569	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧}))
57		0xp 5649	. . . . . . . . . . . . . . . . 17 ⊢ (∅ × {𝑧}) = ∅
58	56, 57	syl6eq 2872	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
59	58	rneqd 5808	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ran ∅)
60		rn0 5796	. . . . . . . . . . . . . . 15 ⊢ ran ∅ = ∅
61	59, 60	syl6eq 2872	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = ∅)
62		0ss 4350	. . . . . . . . . . . . . 14 ⊢ ∅ ⊆ 𝐵
63	61, 62	eqsstrdi 4021	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
64	63	a1d 25	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) = ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
65		rnxp 6027	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
66	65	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) = {𝑧})
67		snssi 4741	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ 𝐵 → {𝑧} ⊆ 𝐵)
68	67	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → {𝑧} ⊆ 𝐵)
69	66, 68	eqsstrd 4005	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∖ ran 𝑔) ≠ ∅ ∧ 𝑧 ∈ 𝐵) → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
70	69	ex 415	. . . . . . . . . . . 12 ⊢ ((𝐴 ∖ ran 𝑔) ≠ ∅ → (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵))
71	64, 70	pm2.61ine 3100	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐵 → ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵)
72		ssequn2 4159	. . . . . . . . . . 11 ⊢ (ran ((𝐴 ∖ ran 𝑔) × {𝑧}) ⊆ 𝐵 ↔ (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
73	71, 72	sylib 220	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐵 → (𝐵 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
74	55, 73	sylan9eqr 2878	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (ran ◡𝑔 ∪ ran ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
75	51, 74	syl5eq 2868	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵)
76		df-fo 6361	. . . . . . . 8 ⊢ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵 ↔ ((◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) Fn 𝐴 ∧ ran (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})) = 𝐵))
77	50, 75, 76	sylanbrc 585	. . . . . . 7 ⊢ ((𝑧 ∈ 𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → (◡𝑔 ∪ ((𝐴 ∖ ran 𝑔) × {𝑧})):𝐴–onto→𝐵)
78		foeq1 6586	. . . . . . . 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 455	. . . . 5 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝐵) → (𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵))
82	81	exlimdv 1934	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ 𝐵) → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵))
83	82	ex 415	. . 3 ⊢ (𝐴 ∈ V → (𝑧 ∈ 𝐵 → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵)))
84	83	exlimdv 1934	. 2 ⊢ (𝐴 ∈ V → (∃𝑧 𝑧 ∈ 𝐵 → (∃𝑔 𝑔:𝐵–1-1→𝐴 → ∃𝑓 𝑓:𝐴–onto→𝐵)))
85	3, 9, 11, 84	syl3c 66	1 ⊢ ((∅ ≺ 𝐵 ∧ 𝐵 ≼ 𝐴) → ∃𝑓 𝑓:𝐴–onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114   ≠ wne 3016  Vcvv 3494   ∖ cdif 3933   ∪ cun 3934   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  {csn 4567   class class class wbr 5066   × cxp 5553  ^◡ccnv 5554  dom cdm 5555  ran crn 5556  Fun wfun 6349   Fn wfn 6350  ⟶wf 6351  –1-1→wf1 6352  –onto→wfo 6353   ≼ cdom 8507   ≺ csdm 8508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512

This theorem is referenced by:  pwdom  8669  fodomfib  8798  domwdom  9038  iunfictbso  9540  fodomb  9948  brdom3  9950  konigthlem  9990  1stcfb  22053  ovoliunnul  24108  sigapildsys  31421  carsgclctunlem3  31578  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  nnfoctb  41358  caragenunicl  42855