Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ V) |
2 | | 0wdom 8475 |
. . . . . 6
⊢ (𝑌 ∈ V → ∅
≼* 𝑌) |
3 | | breq1 4656 |
. . . . . 6
⊢ (𝑋 = ∅ → (𝑋 ≼* 𝑌 ↔ ∅
≼* 𝑌)) |
4 | 2, 3 | syl5ibrcom 237 |
. . . . 5
⊢ (𝑌 ∈ V → (𝑋 = ∅ → 𝑋 ≼* 𝑌)) |
5 | 4 | imp 445 |
. . . 4
⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → 𝑋 ≼* 𝑌) |
6 | | 0elpw 4834 |
. . . . . . 7
⊢ ∅
∈ 𝒫 𝑌 |
7 | | f1o0 6173 |
. . . . . . . 8
⊢
∅:∅–1-1-onto→∅ |
8 | | f1ofo 6144 |
. . . . . . . 8
⊢
(∅:∅–1-1-onto→∅ →
∅:∅–onto→∅) |
9 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
10 | | foeq1 6111 |
. . . . . . . . 9
⊢ (𝑧 = ∅ → (𝑧:∅–onto→∅ ↔ ∅:∅–onto→∅)) |
11 | 9, 10 | spcev 3300 |
. . . . . . . 8
⊢
(∅:∅–onto→∅ → ∃𝑧 𝑧:∅–onto→∅) |
12 | 7, 8, 11 | mp2b 10 |
. . . . . . 7
⊢
∃𝑧 𝑧:∅–onto→∅ |
13 | | foeq2 6112 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → (𝑧:𝑦–onto→∅ ↔ 𝑧:∅–onto→∅)) |
14 | 13 | exbidv 1850 |
. . . . . . . 8
⊢ (𝑦 = ∅ → (∃𝑧 𝑧:𝑦–onto→∅ ↔ ∃𝑧 𝑧:∅–onto→∅)) |
15 | 14 | rspcev 3309 |
. . . . . . 7
⊢ ((∅
∈ 𝒫 𝑌 ∧
∃𝑧 𝑧:∅–onto→∅) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅) |
16 | 6, 12, 15 | mp2an 708 |
. . . . . 6
⊢
∃𝑦 ∈
𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅ |
17 | | foeq3 6113 |
. . . . . . . 8
⊢ (𝑋 = ∅ → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑦–onto→∅)) |
18 | 17 | exbidv 1850 |
. . . . . . 7
⊢ (𝑋 = ∅ → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑦–onto→∅)) |
19 | 18 | rexbidv 3052 |
. . . . . 6
⊢ (𝑋 = ∅ → (∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→∅)) |
20 | 16, 19 | mpbiri 248 |
. . . . 5
⊢ (𝑋 = ∅ → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋) |
21 | 20 | adantl 482 |
. . . 4
⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋) |
22 | 5, 21 | 2thd 255 |
. . 3
⊢ ((𝑌 ∈ V ∧ 𝑋 = ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) |
23 | | brwdomn0 8474 |
. . . . 5
⊢ (𝑋 ≠ ∅ → (𝑋 ≼* 𝑌 ↔ ∃𝑥 𝑥:𝑌–onto→𝑋)) |
24 | 23 | adantl 482 |
. . . 4
⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑥 𝑥:𝑌–onto→𝑋)) |
25 | | foeq1 6111 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥:𝑌–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋)) |
26 | 25 | cbvexv 2275 |
. . . . . 6
⊢
(∃𝑥 𝑥:𝑌–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋) |
27 | | pwidg 4173 |
. . . . . . . . 9
⊢ (𝑌 ∈ V → 𝑌 ∈ 𝒫 𝑌) |
28 | 27 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧
∃𝑧 𝑧:𝑌–onto→𝑋) → 𝑌 ∈ 𝒫 𝑌) |
29 | | foeq2 6112 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋)) |
30 | 29 | exbidv 1850 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)) |
31 | 30 | rspcev 3309 |
. . . . . . . 8
⊢ ((𝑌 ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:𝑌–onto→𝑋) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋) |
32 | 28, 31 | sylancom 701 |
. . . . . . 7
⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧
∃𝑧 𝑧:𝑌–onto→𝑋) → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋) |
33 | 32 | ex 450 |
. . . . . 6
⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) →
(∃𝑧 𝑧:𝑌–onto→𝑋 → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) |
34 | 26, 33 | syl5bi 232 |
. . . . 5
⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) →
(∃𝑥 𝑥:𝑌–onto→𝑋 → ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) |
35 | | n0 3931 |
. . . . . . . . . . 11
⊢ (𝑋 ≠ ∅ ↔
∃𝑤 𝑤 ∈ 𝑋) |
36 | 35 | biimpi 206 |
. . . . . . . . . 10
⊢ (𝑋 ≠ ∅ →
∃𝑤 𝑤 ∈ 𝑋) |
37 | 36 | ad2antlr 763 |
. . . . . . . . 9
⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ∃𝑤 𝑤 ∈ 𝑋) |
38 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
39 | | difexg 4808 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈ V → (𝑌 ∖ 𝑦) ∈ V) |
40 | | snex 4908 |
. . . . . . . . . . . . . 14
⊢ {𝑤} ∈ V |
41 | | xpexg 6960 |
. . . . . . . . . . . . . 14
⊢ (((𝑌 ∖ 𝑦) ∈ V ∧ {𝑤} ∈ V) → ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V) |
42 | 39, 40, 41 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝑌 ∈ V → ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V) |
43 | | unexg 6959 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ V ∧ ((𝑌 ∖ 𝑦) × {𝑤}) ∈ V) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V) |
44 | 38, 42, 43 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ V → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V) |
45 | 44 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V) |
46 | 45 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V) |
47 | | fofn 6117 |
. . . . . . . . . . . . . . 15
⊢ (𝑧:𝑦–onto→𝑋 → 𝑧 Fn 𝑦) |
48 | 47 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋) → 𝑧 Fn 𝑦) |
49 | 48 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → 𝑧 Fn 𝑦) |
50 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑤 ∈ V |
51 | | fnconstg 6093 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ V → ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦)) |
52 | 50, 51 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦)) |
53 | | disjdif 4040 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅ |
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅) |
55 | | fnun 5997 |
. . . . . . . . . . . . 13
⊢ (((𝑧 Fn 𝑦 ∧ ((𝑌 ∖ 𝑦) × {𝑤}) Fn (𝑌 ∖ 𝑦)) ∧ (𝑦 ∩ (𝑌 ∖ 𝑦)) = ∅) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦))) |
56 | 49, 52, 54, 55 | syl21anc 1325 |
. . . . . . . . . . . 12
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦))) |
57 | | elpwi 4168 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝒫 𝑌 → 𝑦 ⊆ 𝑌) |
58 | | undif 4049 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ 𝑌 ↔ (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌) |
59 | 57, 58 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝒫 𝑌 → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌) |
60 | 59 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑦 ∪ (𝑌 ∖ 𝑦)) = 𝑌) |
62 | 61 | fneq2d 5982 |
. . . . . . . . . . . 12
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌 ∖ 𝑦)) ↔ (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌)) |
63 | 56, 62 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌) |
64 | | rnun 5541 |
. . . . . . . . . . . 12
⊢ ran
(𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) |
65 | | forn 6118 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧:𝑦–onto→𝑋 → ran 𝑧 = 𝑋) |
66 | 65 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ran 𝑧 = 𝑋) |
67 | 66 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran 𝑧 = 𝑋) |
68 | 67 | uneq1d 3766 |
. . . . . . . . . . . . 13
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤}))) |
69 | | fconst6g 6094 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝑋 → ((𝑌 ∖ 𝑦) × {𝑤}):(𝑌 ∖ 𝑦)⟶𝑋) |
70 | | frn 6053 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑌 ∖ 𝑦) × {𝑤}):(𝑌 ∖ 𝑦)⟶𝑋 → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝑋 → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran ((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋) |
73 | | ssequn2 3786 |
. . . . . . . . . . . . . 14
⊢ (ran
((𝑌 ∖ 𝑦) × {𝑤}) ⊆ 𝑋 ↔ (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋) |
74 | 72, 73 | sylib 208 |
. . . . . . . . . . . . 13
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑋 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋) |
75 | 68, 74 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (ran 𝑧 ∪ ran ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋) |
76 | 64, 75 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋) |
77 | | df-fo 5894 |
. . . . . . . . . . 11
⊢ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋 ↔ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) Fn 𝑌 ∧ ran (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) = 𝑋)) |
78 | 63, 76, 77 | sylanbrc 698 |
. . . . . . . . . 10
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋) |
79 | | foeq1 6111 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) → (𝑥:𝑌–onto→𝑋 ↔ (𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋)) |
80 | 79 | spcegv 3294 |
. . . . . . . . . 10
⊢ ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})) ∈ V → ((𝑧 ∪ ((𝑌 ∖ 𝑦) × {𝑤})):𝑌–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋)) |
81 | 46, 78, 80 | sylc 65 |
. . . . . . . . 9
⊢ ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) ∧ 𝑤 ∈ 𝑋) → ∃𝑥 𝑥:𝑌–onto→𝑋) |
82 | 37, 81 | exlimddv 1863 |
. . . . . . . 8
⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌 ∧ 𝑧:𝑦–onto→𝑋)) → ∃𝑥 𝑥:𝑌–onto→𝑋) |
83 | 82 | expr 643 |
. . . . . . 7
⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋)) |
84 | 83 | exlimdv 1861 |
. . . . . 6
⊢ (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (∃𝑧 𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋)) |
85 | 84 | rexlimdva 3031 |
. . . . 5
⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) →
(∃𝑦 ∈ 𝒫
𝑌∃𝑧 𝑧:𝑦–onto→𝑋 → ∃𝑥 𝑥:𝑌–onto→𝑋)) |
86 | 34, 85 | impbid 202 |
. . . 4
⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) →
(∃𝑥 𝑥:𝑌–onto→𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) |
87 | 24, 86 | bitrd 268 |
. . 3
⊢ ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) |
88 | 22, 87 | pm2.61dane 2881 |
. 2
⊢ (𝑌 ∈ V → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) |
89 | 1, 88 | syl 17 |
1
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌∃𝑧 𝑧:𝑦–onto→𝑋)) |