Step | Hyp | Ref
| Expression |
1 | | brdomi 6707 |
. . . . 5
⊢ (𝑦 ≼ 𝑥 → ∃𝑔 𝑔:𝑦–1-1→𝑥) |
2 | 1 | ad2antll 483 |
. . . 4
⊢
((EXMID ∧ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥)) → ∃𝑔 𝑔:𝑦–1-1→𝑥) |
3 | | df-f1 5188 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔:𝑦–1-1→𝑥 ↔ (𝑔:𝑦⟶𝑥 ∧ Fun ◡𝑔)) |
4 | 3 | simprbi 273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:𝑦–1-1→𝑥 → Fun ◡𝑔) |
5 | | vex 2725 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
6 | 5 | fconst 5378 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∖ ran 𝑔) × {𝑧}):(𝑥 ∖ ran 𝑔)⟶{𝑧} |
7 | | ffun 5335 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∖ ran 𝑔) × {𝑧}):(𝑥 ∖ ran 𝑔)⟶{𝑧} → Fun ((𝑥 ∖ ran 𝑔) × {𝑧})) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ Fun
((𝑥 ∖ ran 𝑔) × {𝑧}) |
9 | 4, 8 | jctir 311 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:𝑦–1-1→𝑥 → (Fun ◡𝑔 ∧ Fun ((𝑥 ∖ ran 𝑔) × {𝑧}))) |
10 | | df-rn 4610 |
. . . . . . . . . . . . . . . . . 18
⊢ ran 𝑔 = dom ◡𝑔 |
11 | 10 | eqcomi 2168 |
. . . . . . . . . . . . . . . . 17
⊢ dom ◡𝑔 = ran 𝑔 |
12 | 5 | snm 3691 |
. . . . . . . . . . . . . . . . . 18
⊢
∃𝑤 𝑤 ∈ {𝑧} |
13 | | dmxpm 4819 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑤 𝑤 ∈ {𝑧} → dom ((𝑥 ∖ ran 𝑔) × {𝑧}) = (𝑥 ∖ ran 𝑔)) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ dom
((𝑥 ∖ ran 𝑔) × {𝑧}) = (𝑥 ∖ ran 𝑔) |
15 | 11, 14 | ineq12i 3317 |
. . . . . . . . . . . . . . . 16
⊢ (dom
◡𝑔 ∩ dom ((𝑥 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∩ (𝑥 ∖ ran 𝑔)) |
16 | | disjdif 3477 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑔 ∩ (𝑥 ∖ ran 𝑔)) = ∅ |
17 | 15, 16 | eqtri 2185 |
. . . . . . . . . . . . . . 15
⊢ (dom
◡𝑔 ∩ dom ((𝑥 ∖ ran 𝑔) × {𝑧})) = ∅ |
18 | | funun 5227 |
. . . . . . . . . . . . . . 15
⊢ (((Fun
◡𝑔 ∧ Fun ((𝑥 ∖ ran 𝑔) × {𝑧})) ∧ (dom ◡𝑔 ∩ dom ((𝑥 ∖ ran 𝑔) × {𝑧})) = ∅) → Fun (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧}))) |
19 | 9, 17, 18 | sylancl 410 |
. . . . . . . . . . . . . 14
⊢ (𝑔:𝑦–1-1→𝑥 → Fun (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧}))) |
20 | 19 | adantl 275 |
. . . . . . . . . . . . 13
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → Fun (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧}))) |
21 | | dmun 4806 |
. . . . . . . . . . . . . . 15
⊢ dom
(◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝑥 ∖ ran 𝑔) × {𝑧})) |
22 | 10 | uneq1i 3268 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑔 ∪ dom ((𝑥 ∖ ran 𝑔) × {𝑧})) = (dom ◡𝑔 ∪ dom ((𝑥 ∖ ran 𝑔) × {𝑧})) |
23 | 14 | uneq2i 3269 |
. . . . . . . . . . . . . . 15
⊢ (ran
𝑔 ∪ dom ((𝑥 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝑥 ∖ ran 𝑔)) |
24 | 21, 22, 23 | 3eqtr2i 2191 |
. . . . . . . . . . . . . 14
⊢ dom
(◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) = (ran 𝑔 ∪ (𝑥 ∖ ran 𝑔)) |
25 | | f1rn 5389 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:𝑦–1-1→𝑥 → ran 𝑔 ⊆ 𝑥) |
26 | 25 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → ran 𝑔 ⊆ 𝑥) |
27 | | exmidexmid 4170 |
. . . . . . . . . . . . . . . . 17
⊢
(EXMID → DECID 𝑢 ∈ ran 𝑔) |
28 | 27 | ralrimivw 2538 |
. . . . . . . . . . . . . . . 16
⊢
(EXMID → ∀𝑢 ∈ 𝑥 DECID 𝑢 ∈ ran 𝑔) |
29 | 28 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → ∀𝑢 ∈ 𝑥 DECID 𝑢 ∈ ran 𝑔) |
30 | | undifdcss 6880 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (ran 𝑔 ∪ (𝑥 ∖ ran 𝑔)) ↔ (ran 𝑔 ⊆ 𝑥 ∧ ∀𝑢 ∈ 𝑥 DECID 𝑢 ∈ ran 𝑔)) |
31 | 26, 29, 30 | sylanbrc 414 |
. . . . . . . . . . . . . 14
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → 𝑥 = (ran 𝑔 ∪ (𝑥 ∖ ran 𝑔))) |
32 | 24, 31 | eqtr4id 2216 |
. . . . . . . . . . . . 13
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → dom (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) = 𝑥) |
33 | | df-fn 5186 |
. . . . . . . . . . . . 13
⊢ ((◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) Fn 𝑥 ↔ (Fun (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) ∧ dom (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) = 𝑥)) |
34 | 20, 32, 33 | sylanbrc 414 |
. . . . . . . . . . . 12
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) Fn 𝑥) |
35 | | rnun 5007 |
. . . . . . . . . . . . 13
⊢ ran
(◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) = (ran ◡𝑔 ∪ ran ((𝑥 ∖ ran 𝑔) × {𝑧})) |
36 | | dfdm4 4791 |
. . . . . . . . . . . . . . . 16
⊢ dom 𝑔 = ran ◡𝑔 |
37 | | f1dm 5393 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:𝑦–1-1→𝑥 → dom 𝑔 = 𝑦) |
38 | 36, 37 | eqtr3id 2211 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:𝑦–1-1→𝑥 → ran ◡𝑔 = 𝑦) |
39 | 38 | uneq1d 3271 |
. . . . . . . . . . . . . 14
⊢ (𝑔:𝑦–1-1→𝑥 → (ran ◡𝑔 ∪ ran ((𝑥 ∖ ran 𝑔) × {𝑧})) = (𝑦 ∪ ran ((𝑥 ∖ ran 𝑔) × {𝑧}))) |
40 | | exmidexmid 4170 |
. . . . . . . . . . . . . . . . . 18
⊢
(EXMID → DECID ∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔)) |
41 | | exmiddc 826 |
. . . . . . . . . . . . . . . . . 18
⊢
(DECID ∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) → (∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) ∨ ¬ ∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔))) |
42 | 40, 41 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢
(EXMID → (∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) ∨ ¬ ∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔))) |
43 | | rnxpm 5028 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) = {𝑧}) |
44 | 43 | adantr 274 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) ∧ 𝑧 ∈ 𝑦) → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) = {𝑧}) |
45 | | snssi 3712 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝑦 → {𝑧} ⊆ 𝑦) |
46 | 45 | adantl 275 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) ∧ 𝑧 ∈ 𝑦) → {𝑧} ⊆ 𝑦) |
47 | 44, 46 | eqsstrd 3174 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) ∧ 𝑧 ∈ 𝑦) → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦) |
48 | 47 | ex 114 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) → (𝑧 ∈ 𝑦 → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦)) |
49 | | notm0 3425 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) ↔ (𝑥 ∖ ran 𝑔) = ∅) |
50 | | xpeq1 4613 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∖ ran 𝑔) = ∅ → ((𝑥 ∖ ran 𝑔) × {𝑧}) = (∅ × {𝑧})) |
51 | | 0xp 4679 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∅
× {𝑧}) =
∅ |
52 | 50, 51 | eqtrdi 2213 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∖ ran 𝑔) = ∅ → ((𝑥 ∖ ran 𝑔) × {𝑧}) = ∅) |
53 | 52 | rneqd 4828 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∖ ran 𝑔) = ∅ → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) = ran ∅) |
54 | | rn0 4855 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ran
∅ = ∅ |
55 | 53, 54 | eqtrdi 2213 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∖ ran 𝑔) = ∅ → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) = ∅) |
56 | | 0ss 3443 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∅
⊆ 𝑦 |
57 | 55, 56 | eqsstrdi 3190 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∖ ran 𝑔) = ∅ → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦) |
58 | 57 | a1d 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∖ ran 𝑔) = ∅ → (𝑧 ∈ 𝑦 → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦)) |
59 | 49, 58 | sylbi 120 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) → (𝑧 ∈ 𝑦 → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦)) |
60 | 48, 59 | jaoi 706 |
. . . . . . . . . . . . . . . . 17
⊢
((∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔) ∨ ¬ ∃𝑣 𝑣 ∈ (𝑥 ∖ ran 𝑔)) → (𝑧 ∈ 𝑦 → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦)) |
61 | 42, 60 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢
(EXMID → (𝑧 ∈ 𝑦 → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦)) |
62 | 61 | imp 123 |
. . . . . . . . . . . . . . 15
⊢
((EXMID ∧ 𝑧 ∈ 𝑦) → ran ((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦) |
63 | | ssequn2 3291 |
. . . . . . . . . . . . . . 15
⊢ (ran
((𝑥 ∖ ran 𝑔) × {𝑧}) ⊆ 𝑦 ↔ (𝑦 ∪ ran ((𝑥 ∖ ran 𝑔) × {𝑧})) = 𝑦) |
64 | 62, 63 | sylib 121 |
. . . . . . . . . . . . . 14
⊢
((EXMID ∧ 𝑧 ∈ 𝑦) → (𝑦 ∪ ran ((𝑥 ∖ ran 𝑔) × {𝑧})) = 𝑦) |
65 | 39, 64 | sylan9eqr 2219 |
. . . . . . . . . . . . 13
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → (ran ◡𝑔 ∪ ran ((𝑥 ∖ ran 𝑔) × {𝑧})) = 𝑦) |
66 | 35, 65 | syl5eq 2209 |
. . . . . . . . . . . 12
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → ran (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) = 𝑦) |
67 | | df-fo 5189 |
. . . . . . . . . . . 12
⊢ ((◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})):𝑥–onto→𝑦 ↔ ((◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) Fn 𝑥 ∧ ran (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) = 𝑦)) |
68 | 34, 66, 67 | sylanbrc 414 |
. . . . . . . . . . 11
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})):𝑥–onto→𝑦) |
69 | | vex 2725 |
. . . . . . . . . . . . . 14
⊢ 𝑔 ∈ V |
70 | 69 | cnvex 5137 |
. . . . . . . . . . . . 13
⊢ ◡𝑔 ∈ V |
71 | | vex 2725 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
72 | | difexg 4118 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ V → (𝑥 ∖ ran 𝑔) ∈ V) |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∖ ran 𝑔) ∈ V |
74 | 5 | snex 4159 |
. . . . . . . . . . . . . 14
⊢ {𝑧} ∈ V |
75 | 73, 74 | xpex 4714 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∖ ran 𝑔) × {𝑧}) ∈ V |
76 | 70, 75 | unex 4414 |
. . . . . . . . . . . 12
⊢ (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) ∈ V |
77 | | foeq1 5401 |
. . . . . . . . . . . 12
⊢ (𝑓 = (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})) → (𝑓:𝑥–onto→𝑦 ↔ (◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})):𝑥–onto→𝑦)) |
78 | 76, 77 | spcev 2817 |
. . . . . . . . . . 11
⊢ ((◡𝑔 ∪ ((𝑥 ∖ ran 𝑔) × {𝑧})):𝑥–onto→𝑦 → ∃𝑓 𝑓:𝑥–onto→𝑦) |
79 | 68, 78 | syl 14 |
. . . . . . . . . 10
⊢
(((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) |
80 | 79 | an32s 558 |
. . . . . . . . 9
⊢
(((EXMID ∧ 𝑔:𝑦–1-1→𝑥) ∧ 𝑧 ∈ 𝑦) → ∃𝑓 𝑓:𝑥–onto→𝑦) |
81 | 80 | ex 114 |
. . . . . . . 8
⊢
((EXMID ∧ 𝑔:𝑦–1-1→𝑥) → (𝑧 ∈ 𝑦 → ∃𝑓 𝑓:𝑥–onto→𝑦)) |
82 | 81 | exlimdv 1806 |
. . . . . . 7
⊢
((EXMID ∧ 𝑔:𝑦–1-1→𝑥) → (∃𝑧 𝑧 ∈ 𝑦 → ∃𝑓 𝑓:𝑥–onto→𝑦)) |
83 | 82 | imp 123 |
. . . . . 6
⊢
(((EXMID ∧ 𝑔:𝑦–1-1→𝑥) ∧ ∃𝑧 𝑧 ∈ 𝑦) → ∃𝑓 𝑓:𝑥–onto→𝑦) |
84 | 83 | an32s 558 |
. . . . 5
⊢
(((EXMID ∧ ∃𝑧 𝑧 ∈ 𝑦) ∧ 𝑔:𝑦–1-1→𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) |
85 | 84 | adantlrr 475 |
. . . 4
⊢
(((EXMID ∧ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥)) ∧ 𝑔:𝑦–1-1→𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) |
86 | 2, 85 | exlimddv 1885 |
. . 3
⊢
((EXMID ∧ (∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥)) → ∃𝑓 𝑓:𝑥–onto→𝑦) |
87 | 86 | ex 114 |
. 2
⊢
(EXMID → ((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)) |
88 | 87 | alrimivv 1862 |
1
⊢
(EXMID → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)) |