Step | Hyp | Ref
| Expression |
1 | | elex 3492 |
. 2
⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ V) |
2 | | relwdom 9560 |
. . . . 5
⊢ Rel
≼* |
3 | 2 | brrelex1i 5732 |
. . . 4
⊢ (𝑋 ≼* 𝑌 → 𝑋 ∈ V) |
4 | 3 | a1i 11 |
. . 3
⊢ (𝑌 ∈ V → (𝑋 ≼* 𝑌 → 𝑋 ∈ V)) |
5 | | 0ex 5307 |
. . . . . 6
⊢ ∅
∈ V |
6 | | eleq1a 2828 |
. . . . . 6
⊢ (∅
∈ V → (𝑋 =
∅ → 𝑋 ∈
V)) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ (𝑋 = ∅ → 𝑋 ∈ V) |
8 | | forn 6808 |
. . . . . . 7
⊢ (𝑧:𝑌–onto→𝑋 → ran 𝑧 = 𝑋) |
9 | | vex 3478 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
10 | 9 | rnex 7902 |
. . . . . . 7
⊢ ran 𝑧 ∈ V |
11 | 8, 10 | eqeltrrdi 2842 |
. . . . . 6
⊢ (𝑧:𝑌–onto→𝑋 → 𝑋 ∈ V) |
12 | 11 | exlimiv 1933 |
. . . . 5
⊢
(∃𝑧 𝑧:𝑌–onto→𝑋 → 𝑋 ∈ V) |
13 | 7, 12 | jaoi 855 |
. . . 4
⊢ ((𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋) → 𝑋 ∈ V) |
14 | 13 | a1i 11 |
. . 3
⊢ (𝑌 ∈ V → ((𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋) → 𝑋 ∈ V)) |
15 | | eqeq1 2736 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 = ∅ ↔ 𝑋 = ∅)) |
16 | | foeq3 6803 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑧:𝑦–onto→𝑥 ↔ 𝑧:𝑦–onto→𝑋)) |
17 | 16 | exbidv 1924 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑧 𝑧:𝑦–onto→𝑥 ↔ ∃𝑧 𝑧:𝑦–onto→𝑋)) |
18 | 15, 17 | orbi12d 917 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥) ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑋))) |
19 | | foeq2 6802 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (𝑧:𝑦–onto→𝑋 ↔ 𝑧:𝑌–onto→𝑋)) |
20 | 19 | exbidv 1924 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (∃𝑧 𝑧:𝑦–onto→𝑋 ↔ ∃𝑧 𝑧:𝑌–onto→𝑋)) |
21 | 20 | orbi2d 914 |
. . . . 5
⊢ (𝑦 = 𝑌 → ((𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑋) ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))) |
22 | | df-wdom 9559 |
. . . . 5
⊢
≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)} |
23 | 18, 21, 22 | brabg 5539 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))) |
24 | 23 | expcom 414 |
. . 3
⊢ (𝑌 ∈ V → (𝑋 ∈ V → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋)))) |
25 | 4, 14, 24 | pm5.21ndd 380 |
. 2
⊢ (𝑌 ∈ V → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))) |
26 | 1, 25 | syl 17 |
1
⊢ (𝑌 ∈ 𝑉 → (𝑋 ≼* 𝑌 ↔ (𝑋 = ∅ ∨ ∃𝑧 𝑧:𝑌–onto→𝑋))) |