Step | Hyp | Ref
| Expression |
1 | | reldom 8561 |
. . . . 5
⊢ Rel
≼ |
2 | 1 | brrelex2i 5580 |
. . . 4
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) |
3 | | djudoml 9684 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ≼ (𝐴 ⊔ 𝐴)) |
4 | 2, 2, 3 | syl2anc 587 |
. . 3
⊢ (ω
≼ 𝐴 → 𝐴 ≼ (𝐴 ⊔ 𝐴)) |
5 | | domtr 8608 |
. . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ (𝐴 ⊔ 𝐴)) → ω ≼ (𝐴 ⊔ 𝐴)) |
6 | 4, 5 | mpdan 687 |
. 2
⊢ (ω
≼ 𝐴 → ω
≼ (𝐴 ⊔ 𝐴)) |
7 | 1 | brrelex2i 5580 |
. . . 4
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → (𝐴 ⊔ 𝐴) ∈ V) |
8 | | anidm 568 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) ↔ 𝐴 ∈ V) |
9 | | djuexb 9411 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐴 ⊔ 𝐴) ∈ V) |
10 | 8, 9 | bitr3i 280 |
. . . 4
⊢ (𝐴 ∈ V ↔ (𝐴 ⊔ 𝐴) ∈ V) |
11 | 7, 10 | sylibr 237 |
. . 3
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → 𝐴 ∈ V) |
12 | | domeng 8569 |
. . . . 5
⊢ ((𝐴 ⊔ 𝐴) ∈ V → (ω ≼ (𝐴 ⊔ 𝐴) ↔ ∃𝑥(ω ≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)))) |
13 | 7, 12 | syl 17 |
. . . 4
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → (ω ≼ (𝐴 ⊔ 𝐴) ↔ ∃𝑥(ω ≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)))) |
14 | 13 | ibi 270 |
. . 3
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → ∃𝑥(ω ≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴))) |
15 | | indi 4164 |
. . . . . . 7
⊢ (𝑥 ∩ (({∅} × 𝐴) ∪ ({1o} ×
𝐴))) = ((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) |
16 | | simpr 488 |
. . . . . . . . 9
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → 𝑥 ⊆ (𝐴 ⊔ 𝐴)) |
17 | | df-dju 9403 |
. . . . . . . . 9
⊢ (𝐴 ⊔ 𝐴) = (({∅} × 𝐴) ∪ ({1o} × 𝐴)) |
18 | 16, 17 | sseqtrdi 3927 |
. . . . . . . 8
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → 𝑥 ⊆ (({∅} × 𝐴) ∪ ({1o} ×
𝐴))) |
19 | | df-ss 3860 |
. . . . . . . 8
⊢ (𝑥 ⊆ (({∅} ×
𝐴) ∪ ({1o}
× 𝐴)) ↔ (𝑥 ∩ (({∅} × 𝐴) ∪ ({1o} ×
𝐴))) = 𝑥) |
20 | 18, 19 | sylib 221 |
. . . . . . 7
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → (𝑥 ∩ (({∅} × 𝐴) ∪ ({1o} × 𝐴))) = 𝑥) |
21 | 15, 20 | eqtr3id 2787 |
. . . . . 6
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → ((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) = 𝑥) |
22 | | ensym 8604 |
. . . . . . 7
⊢ (ω
≈ 𝑥 → 𝑥 ≈
ω) |
23 | 22 | adantr 484 |
. . . . . 6
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → 𝑥 ≈ ω) |
24 | 21, 23 | eqbrtrd 5052 |
. . . . 5
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → ((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) ≈
ω) |
25 | | cdainflem 9687 |
. . . . . 6
⊢ (((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) ≈ ω →
((𝑥 ∩ ({∅}
× 𝐴)) ≈ ω
∨ (𝑥 ∩
({1o} × 𝐴)) ≈ ω)) |
26 | | snex 5298 |
. . . . . . . . . . 11
⊢ {∅}
∈ V |
27 | | xpexg 7491 |
. . . . . . . . . . 11
⊢
(({∅} ∈ V ∧ 𝐴 ∈ V) → ({∅} × 𝐴) ∈ V) |
28 | 26, 27 | mpan 690 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → ({∅}
× 𝐴) ∈
V) |
29 | | inss2 4120 |
. . . . . . . . . 10
⊢ (𝑥 ∩ ({∅} × 𝐴)) ⊆ ({∅} ×
𝐴) |
30 | | ssdomg 8601 |
. . . . . . . . . 10
⊢
(({∅} × 𝐴) ∈ V → ((𝑥 ∩ ({∅} × 𝐴)) ⊆ ({∅} × 𝐴) → (𝑥 ∩ ({∅} × 𝐴)) ≼ ({∅} × 𝐴))) |
31 | 28, 29, 30 | mpisyl 21 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑥 ∩ ({∅} × 𝐴)) ≼ ({∅} ×
𝐴)) |
32 | | 0ex 5175 |
. . . . . . . . . 10
⊢ ∅
∈ V |
33 | | xpsnen2g 8659 |
. . . . . . . . . 10
⊢ ((∅
∈ V ∧ 𝐴 ∈ V)
→ ({∅} × 𝐴) ≈ 𝐴) |
34 | 32, 33 | mpan 690 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → ({∅}
× 𝐴) ≈ 𝐴) |
35 | | domentr 8614 |
. . . . . . . . 9
⊢ (((𝑥 ∩ ({∅} × 𝐴)) ≼ ({∅} ×
𝐴) ∧ ({∅} ×
𝐴) ≈ 𝐴) → (𝑥 ∩ ({∅} × 𝐴)) ≼ 𝐴) |
36 | 31, 34, 35 | syl2anc 587 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝑥 ∩ ({∅} × 𝐴)) ≼ 𝐴) |
37 | | domen1 8709 |
. . . . . . . 8
⊢ ((𝑥 ∩ ({∅} × 𝐴)) ≈ ω →
((𝑥 ∩ ({∅}
× 𝐴)) ≼ 𝐴 ↔ ω ≼ 𝐴)) |
38 | 36, 37 | syl5ibcom 248 |
. . . . . . 7
⊢ (𝐴 ∈ V → ((𝑥 ∩ ({∅} × 𝐴)) ≈ ω →
ω ≼ 𝐴)) |
39 | | snex 5298 |
. . . . . . . . . . 11
⊢
{1o} ∈ V |
40 | | xpexg 7491 |
. . . . . . . . . . 11
⊢
(({1o} ∈ V ∧ 𝐴 ∈ V) → ({1o} ×
𝐴) ∈
V) |
41 | 39, 40 | mpan 690 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V →
({1o} × 𝐴)
∈ V) |
42 | | inss2 4120 |
. . . . . . . . . 10
⊢ (𝑥 ∩ ({1o} ×
𝐴)) ⊆
({1o} × 𝐴) |
43 | | ssdomg 8601 |
. . . . . . . . . 10
⊢
(({1o} × 𝐴) ∈ V → ((𝑥 ∩ ({1o} × 𝐴)) ⊆ ({1o}
× 𝐴) → (𝑥 ∩ ({1o} ×
𝐴)) ≼
({1o} × 𝐴))) |
44 | 41, 42, 43 | mpisyl 21 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑥 ∩ ({1o} ×
𝐴)) ≼
({1o} × 𝐴)) |
45 | | 1on 8138 |
. . . . . . . . . 10
⊢
1o ∈ On |
46 | | xpsnen2g 8659 |
. . . . . . . . . 10
⊢
((1o ∈ On ∧ 𝐴 ∈ V) → ({1o} ×
𝐴) ≈ 𝐴) |
47 | 45, 46 | mpan 690 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
({1o} × 𝐴)
≈ 𝐴) |
48 | | domentr 8614 |
. . . . . . . . 9
⊢ (((𝑥 ∩ ({1o} ×
𝐴)) ≼
({1o} × 𝐴)
∧ ({1o} × 𝐴) ≈ 𝐴) → (𝑥 ∩ ({1o} × 𝐴)) ≼ 𝐴) |
49 | 44, 47, 48 | syl2anc 587 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝑥 ∩ ({1o} ×
𝐴)) ≼ 𝐴) |
50 | | domen1 8709 |
. . . . . . . 8
⊢ ((𝑥 ∩ ({1o} ×
𝐴)) ≈ ω →
((𝑥 ∩ ({1o}
× 𝐴)) ≼ 𝐴 ↔ ω ≼ 𝐴)) |
51 | 49, 50 | syl5ibcom 248 |
. . . . . . 7
⊢ (𝐴 ∈ V → ((𝑥 ∩ ({1o} ×
𝐴)) ≈ ω →
ω ≼ 𝐴)) |
52 | 38, 51 | jaod 858 |
. . . . . 6
⊢ (𝐴 ∈ V → (((𝑥 ∩ ({∅} × 𝐴)) ≈ ω ∨ (𝑥 ∩ ({1o} ×
𝐴)) ≈ ω) →
ω ≼ 𝐴)) |
53 | 25, 52 | syl5 34 |
. . . . 5
⊢ (𝐴 ∈ V → (((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) ≈ ω →
ω ≼ 𝐴)) |
54 | 24, 53 | syl5 34 |
. . . 4
⊢ (𝐴 ∈ V → ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → ω ≼ 𝐴)) |
55 | 54 | exlimdv 1940 |
. . 3
⊢ (𝐴 ∈ V → (∃𝑥(ω ≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → ω ≼ 𝐴)) |
56 | 11, 14, 55 | sylc 65 |
. 2
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → ω ≼ 𝐴) |
57 | 6, 56 | impbii 212 |
1
⊢ (ω
≼ 𝐴 ↔ ω
≼ (𝐴 ⊔ 𝐴)) |