| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reldom 8992 | . . . . 5
⊢ Rel
≼ | 
| 2 | 1 | brrelex2i 5741 | . . . 4
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) | 
| 3 |  | djudoml 10226 | . . . 4
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ≼ (𝐴 ⊔ 𝐴)) | 
| 4 | 2, 2, 3 | syl2anc 584 | . . 3
⊢ (ω
≼ 𝐴 → 𝐴 ≼ (𝐴 ⊔ 𝐴)) | 
| 5 |  | domtr 9048 | . . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐴 ≼ (𝐴 ⊔ 𝐴)) → ω ≼ (𝐴 ⊔ 𝐴)) | 
| 6 | 4, 5 | mpdan 687 | . 2
⊢ (ω
≼ 𝐴 → ω
≼ (𝐴 ⊔ 𝐴)) | 
| 7 | 1 | brrelex2i 5741 | . . . 4
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → (𝐴 ⊔ 𝐴) ∈ V) | 
| 8 |  | anidm 564 | . . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) ↔ 𝐴 ∈ V) | 
| 9 |  | djuexb 9950 | . . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐴 ⊔ 𝐴) ∈ V) | 
| 10 | 8, 9 | bitr3i 277 | . . . 4
⊢ (𝐴 ∈ V ↔ (𝐴 ⊔ 𝐴) ∈ V) | 
| 11 | 7, 10 | sylibr 234 | . . 3
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → 𝐴 ∈ V) | 
| 12 |  | domeng 9004 | . . . . 5
⊢ ((𝐴 ⊔ 𝐴) ∈ V → (ω ≼ (𝐴 ⊔ 𝐴) ↔ ∃𝑥(ω ≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)))) | 
| 13 | 7, 12 | syl 17 | . . . 4
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → (ω ≼ (𝐴 ⊔ 𝐴) ↔ ∃𝑥(ω ≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)))) | 
| 14 | 13 | ibi 267 | . . 3
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → ∃𝑥(ω ≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴))) | 
| 15 |  | indi 4283 | . . . . . . 7
⊢ (𝑥 ∩ (({∅} × 𝐴) ∪ ({1o} ×
𝐴))) = ((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) | 
| 16 |  | simpr 484 | . . . . . . . . 9
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → 𝑥 ⊆ (𝐴 ⊔ 𝐴)) | 
| 17 |  | df-dju 9942 | . . . . . . . . 9
⊢ (𝐴 ⊔ 𝐴) = (({∅} × 𝐴) ∪ ({1o} × 𝐴)) | 
| 18 | 16, 17 | sseqtrdi 4023 | . . . . . . . 8
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → 𝑥 ⊆ (({∅} × 𝐴) ∪ ({1o} ×
𝐴))) | 
| 19 |  | dfss2 3968 | . . . . . . . 8
⊢ (𝑥 ⊆ (({∅} ×
𝐴) ∪ ({1o}
× 𝐴)) ↔ (𝑥 ∩ (({∅} × 𝐴) ∪ ({1o} ×
𝐴))) = 𝑥) | 
| 20 | 18, 19 | sylib 218 | . . . . . . 7
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → (𝑥 ∩ (({∅} × 𝐴) ∪ ({1o} × 𝐴))) = 𝑥) | 
| 21 | 15, 20 | eqtr3id 2790 | . . . . . 6
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → ((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) = 𝑥) | 
| 22 |  | ensym 9044 | . . . . . . 7
⊢ (ω
≈ 𝑥 → 𝑥 ≈
ω) | 
| 23 | 22 | adantr 480 | . . . . . 6
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → 𝑥 ≈ ω) | 
| 24 | 21, 23 | eqbrtrd 5164 | . . . . 5
⊢ ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → ((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) ≈
ω) | 
| 25 |  | cdainflem 10229 | . . . . . 6
⊢ (((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) ≈ ω →
((𝑥 ∩ ({∅}
× 𝐴)) ≈ ω
∨ (𝑥 ∩
({1o} × 𝐴)) ≈ ω)) | 
| 26 |  | snex 5435 | . . . . . . . . . . 11
⊢ {∅}
∈ V | 
| 27 |  | xpexg 7771 | . . . . . . . . . . 11
⊢
(({∅} ∈ V ∧ 𝐴 ∈ V) → ({∅} × 𝐴) ∈ V) | 
| 28 | 26, 27 | mpan 690 | . . . . . . . . . 10
⊢ (𝐴 ∈ V → ({∅}
× 𝐴) ∈
V) | 
| 29 |  | inss2 4237 | . . . . . . . . . 10
⊢ (𝑥 ∩ ({∅} × 𝐴)) ⊆ ({∅} ×
𝐴) | 
| 30 |  | ssdomg 9041 | . . . . . . . . . 10
⊢
(({∅} × 𝐴) ∈ V → ((𝑥 ∩ ({∅} × 𝐴)) ⊆ ({∅} × 𝐴) → (𝑥 ∩ ({∅} × 𝐴)) ≼ ({∅} × 𝐴))) | 
| 31 | 28, 29, 30 | mpisyl 21 | . . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑥 ∩ ({∅} × 𝐴)) ≼ ({∅} ×
𝐴)) | 
| 32 |  | 0ex 5306 | . . . . . . . . . 10
⊢ ∅
∈ V | 
| 33 |  | xpsnen2g 9106 | . . . . . . . . . 10
⊢ ((∅
∈ V ∧ 𝐴 ∈ V)
→ ({∅} × 𝐴) ≈ 𝐴) | 
| 34 | 32, 33 | mpan 690 | . . . . . . . . 9
⊢ (𝐴 ∈ V → ({∅}
× 𝐴) ≈ 𝐴) | 
| 35 |  | domentr 9054 | . . . . . . . . 9
⊢ (((𝑥 ∩ ({∅} × 𝐴)) ≼ ({∅} ×
𝐴) ∧ ({∅} ×
𝐴) ≈ 𝐴) → (𝑥 ∩ ({∅} × 𝐴)) ≼ 𝐴) | 
| 36 | 31, 34, 35 | syl2anc 584 | . . . . . . . 8
⊢ (𝐴 ∈ V → (𝑥 ∩ ({∅} × 𝐴)) ≼ 𝐴) | 
| 37 |  | domen1 9160 | . . . . . . . 8
⊢ ((𝑥 ∩ ({∅} × 𝐴)) ≈ ω →
((𝑥 ∩ ({∅}
× 𝐴)) ≼ 𝐴 ↔ ω ≼ 𝐴)) | 
| 38 | 36, 37 | syl5ibcom 245 | . . . . . . 7
⊢ (𝐴 ∈ V → ((𝑥 ∩ ({∅} × 𝐴)) ≈ ω →
ω ≼ 𝐴)) | 
| 39 |  | snex 5435 | . . . . . . . . . . 11
⊢
{1o} ∈ V | 
| 40 |  | xpexg 7771 | . . . . . . . . . . 11
⊢
(({1o} ∈ V ∧ 𝐴 ∈ V) → ({1o} ×
𝐴) ∈
V) | 
| 41 | 39, 40 | mpan 690 | . . . . . . . . . 10
⊢ (𝐴 ∈ V →
({1o} × 𝐴)
∈ V) | 
| 42 |  | inss2 4237 | . . . . . . . . . 10
⊢ (𝑥 ∩ ({1o} ×
𝐴)) ⊆
({1o} × 𝐴) | 
| 43 |  | ssdomg 9041 | . . . . . . . . . 10
⊢
(({1o} × 𝐴) ∈ V → ((𝑥 ∩ ({1o} × 𝐴)) ⊆ ({1o}
× 𝐴) → (𝑥 ∩ ({1o} ×
𝐴)) ≼
({1o} × 𝐴))) | 
| 44 | 41, 42, 43 | mpisyl 21 | . . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑥 ∩ ({1o} ×
𝐴)) ≼
({1o} × 𝐴)) | 
| 45 |  | 1on 8519 | . . . . . . . . . 10
⊢
1o ∈ On | 
| 46 |  | xpsnen2g 9106 | . . . . . . . . . 10
⊢
((1o ∈ On ∧ 𝐴 ∈ V) → ({1o} ×
𝐴) ≈ 𝐴) | 
| 47 | 45, 46 | mpan 690 | . . . . . . . . 9
⊢ (𝐴 ∈ V →
({1o} × 𝐴)
≈ 𝐴) | 
| 48 |  | domentr 9054 | . . . . . . . . 9
⊢ (((𝑥 ∩ ({1o} ×
𝐴)) ≼
({1o} × 𝐴)
∧ ({1o} × 𝐴) ≈ 𝐴) → (𝑥 ∩ ({1o} × 𝐴)) ≼ 𝐴) | 
| 49 | 44, 47, 48 | syl2anc 584 | . . . . . . . 8
⊢ (𝐴 ∈ V → (𝑥 ∩ ({1o} ×
𝐴)) ≼ 𝐴) | 
| 50 |  | domen1 9160 | . . . . . . . 8
⊢ ((𝑥 ∩ ({1o} ×
𝐴)) ≈ ω →
((𝑥 ∩ ({1o}
× 𝐴)) ≼ 𝐴 ↔ ω ≼ 𝐴)) | 
| 51 | 49, 50 | syl5ibcom 245 | . . . . . . 7
⊢ (𝐴 ∈ V → ((𝑥 ∩ ({1o} ×
𝐴)) ≈ ω →
ω ≼ 𝐴)) | 
| 52 | 38, 51 | jaod 859 | . . . . . 6
⊢ (𝐴 ∈ V → (((𝑥 ∩ ({∅} × 𝐴)) ≈ ω ∨ (𝑥 ∩ ({1o} ×
𝐴)) ≈ ω) →
ω ≼ 𝐴)) | 
| 53 | 25, 52 | syl5 34 | . . . . 5
⊢ (𝐴 ∈ V → (((𝑥 ∩ ({∅} × 𝐴)) ∪ (𝑥 ∩ ({1o} × 𝐴))) ≈ ω →
ω ≼ 𝐴)) | 
| 54 | 24, 53 | syl5 34 | . . . 4
⊢ (𝐴 ∈ V → ((ω
≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → ω ≼ 𝐴)) | 
| 55 | 54 | exlimdv 1932 | . . 3
⊢ (𝐴 ∈ V → (∃𝑥(ω ≈ 𝑥 ∧ 𝑥 ⊆ (𝐴 ⊔ 𝐴)) → ω ≼ 𝐴)) | 
| 56 | 11, 14, 55 | sylc 65 | . 2
⊢ (ω
≼ (𝐴 ⊔ 𝐴) → ω ≼ 𝐴) | 
| 57 | 6, 56 | impbii 209 | 1
⊢ (ω
≼ 𝐴 ↔ ω
≼ (𝐴 ⊔ 𝐴)) |