| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | wofi 9325 | . . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴) | 
| 2 |  | cnvso 6308 | . . . 4
⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴) | 
| 3 |  | wofi 9325 | . . . 4
⊢ ((◡𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ◡𝑅 We 𝐴) | 
| 4 | 2, 3 | sylanb 581 | . . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ◡𝑅 We 𝐴) | 
| 5 | 1, 4 | jca 511 | . 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴)) | 
| 6 |  | weso 5676 | . . . 4
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) | 
| 7 | 6 | adantr 480 | . . 3
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → 𝑅 Or 𝐴) | 
| 8 |  | peano2 7912 | . . . . . . . . 9
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) | 
| 9 |  | sucidg 6465 | . . . . . . . . 9
⊢ (𝑦 ∈ ω → 𝑦 ∈ suc 𝑦) | 
| 10 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑧 ∈ V | 
| 11 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑦 ∈ V | 
| 12 | 10, 11 | brcnv 5893 | . . . . . . . . . . . 12
⊢ (𝑧◡ E 𝑦 ↔ 𝑦 E 𝑧) | 
| 13 |  | epel 5587 | . . . . . . . . . . . 12
⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧) | 
| 14 | 12, 13 | bitri 275 | . . . . . . . . . . 11
⊢ (𝑧◡ E 𝑦 ↔ 𝑦 ∈ 𝑧) | 
| 15 |  | eleq2 2830 | . . . . . . . . . . 11
⊢ (𝑧 = suc 𝑦 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ suc 𝑦)) | 
| 16 | 14, 15 | bitrid 283 | . . . . . . . . . 10
⊢ (𝑧 = suc 𝑦 → (𝑧◡ E
𝑦 ↔ 𝑦 ∈ suc 𝑦)) | 
| 17 | 16 | rspcev 3622 | . . . . . . . . 9
⊢ ((suc
𝑦 ∈ ω ∧
𝑦 ∈ suc 𝑦) → ∃𝑧 ∈ ω 𝑧◡ E 𝑦) | 
| 18 | 8, 9, 17 | syl2anc 584 | . . . . . . . 8
⊢ (𝑦 ∈ ω →
∃𝑧 ∈ ω
𝑧◡ E 𝑦) | 
| 19 |  | dfrex2 3073 | . . . . . . . 8
⊢
(∃𝑧 ∈
ω 𝑧◡ E 𝑦 ↔ ¬ ∀𝑧 ∈ ω ¬ 𝑧◡ E
𝑦) | 
| 20 | 18, 19 | sylib 218 | . . . . . . 7
⊢ (𝑦 ∈ ω → ¬
∀𝑧 ∈ ω
¬ 𝑧◡ E 𝑦) | 
| 21 | 20 | nrex 3074 | . . . . . 6
⊢  ¬
∃𝑦 ∈ ω
∀𝑧 ∈ ω
¬ 𝑧◡ E 𝑦 | 
| 22 |  | ordom 7897 | . . . . . . . 8
⊢ Ord
ω | 
| 23 |  | eqid 2737 | . . . . . . . . 9
⊢
OrdIso(𝑅, 𝐴) = OrdIso(𝑅, 𝐴) | 
| 24 | 23 | oicl 9569 | . . . . . . . 8
⊢ Ord dom
OrdIso(𝑅, 𝐴) | 
| 25 |  | ordtri1 6417 | . . . . . . . 8
⊢ ((Ord
ω ∧ Ord dom OrdIso(𝑅, 𝐴)) → (ω ⊆ dom OrdIso(𝑅, 𝐴) ↔ ¬ dom OrdIso(𝑅, 𝐴) ∈ ω)) | 
| 26 | 22, 24, 25 | mp2an 692 | . . . . . . 7
⊢ (ω
⊆ dom OrdIso(𝑅, 𝐴) ↔ ¬ dom OrdIso(𝑅, 𝐴) ∈ ω) | 
| 27 |  | wofib.1 | . . . . . . . . . . 11
⊢ 𝐴 ∈ V | 
| 28 | 23 | oion 9576 | . . . . . . . . . . 11
⊢ (𝐴 ∈ V → dom
OrdIso(𝑅, 𝐴) ∈ On) | 
| 29 | 27, 28 | mp1i 13 | . . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) ∧ ω ⊆ dom OrdIso(𝑅, 𝐴)) → dom OrdIso(𝑅, 𝐴) ∈ On) | 
| 30 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) ∧ ω ⊆ dom OrdIso(𝑅, 𝐴)) → ω ⊆ dom OrdIso(𝑅, 𝐴)) | 
| 31 | 29, 30 | ssexd 5324 | . . . . . . . . 9
⊢ (((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) ∧ ω ⊆ dom OrdIso(𝑅, 𝐴)) → ω ∈ V) | 
| 32 | 23 | oiiso 9577 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴) → OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴)) | 
| 33 | 27, 32 | mpan 690 | . . . . . . . . . . . 12
⊢ (𝑅 We 𝐴 → OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴)) | 
| 34 |  | isocnv2 7351 | . . . . . . . . . . . 12
⊢
(OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴) ↔ OrdIso(𝑅, 𝐴) Isom ◡ E , ◡𝑅(dom OrdIso(𝑅, 𝐴), 𝐴)) | 
| 35 | 33, 34 | sylib 218 | . . . . . . . . . . 11
⊢ (𝑅 We 𝐴 → OrdIso(𝑅, 𝐴) Isom ◡ E , ◡𝑅(dom OrdIso(𝑅, 𝐴), 𝐴)) | 
| 36 |  | wefr 5675 | . . . . . . . . . . 11
⊢ (◡𝑅 We 𝐴 → ◡𝑅 Fr 𝐴) | 
| 37 |  | isofr 7362 | . . . . . . . . . . . 12
⊢
(OrdIso(𝑅, 𝐴) Isom ◡ E , ◡𝑅(dom OrdIso(𝑅, 𝐴), 𝐴) → (◡ E Fr dom OrdIso(𝑅, 𝐴) ↔ ◡𝑅 Fr 𝐴)) | 
| 38 | 37 | biimpar 477 | . . . . . . . . . . 11
⊢
((OrdIso(𝑅, 𝐴) Isom ◡ E , ◡𝑅(dom OrdIso(𝑅, 𝐴), 𝐴) ∧ ◡𝑅 Fr 𝐴) → ◡ E Fr dom OrdIso(𝑅, 𝐴)) | 
| 39 | 35, 36, 38 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → ◡ E Fr dom OrdIso(𝑅, 𝐴)) | 
| 40 | 39 | adantr 480 | . . . . . . . . 9
⊢ (((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) ∧ ω ⊆ dom OrdIso(𝑅, 𝐴)) → ◡ E Fr dom OrdIso(𝑅, 𝐴)) | 
| 41 |  | 1onn 8678 | . . . . . . . . . 10
⊢
1o ∈ ω | 
| 42 |  | ne0i 4341 | . . . . . . . . . 10
⊢
(1o ∈ ω → ω ≠
∅) | 
| 43 | 41, 42 | mp1i 13 | . . . . . . . . 9
⊢ (((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) ∧ ω ⊆ dom OrdIso(𝑅, 𝐴)) → ω ≠
∅) | 
| 44 |  | fri 5642 | . . . . . . . . 9
⊢
(((ω ∈ V ∧ ◡ E Fr
dom OrdIso(𝑅, 𝐴)) ∧ (ω ⊆ dom
OrdIso(𝑅, 𝐴) ∧ ω ≠ ∅)) →
∃𝑦 ∈ ω
∀𝑧 ∈ ω
¬ 𝑧◡ E 𝑦) | 
| 45 | 31, 40, 30, 43, 44 | syl22anc 839 | . . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) ∧ ω ⊆ dom OrdIso(𝑅, 𝐴)) → ∃𝑦 ∈ ω ∀𝑧 ∈ ω ¬ 𝑧◡ E
𝑦) | 
| 46 | 45 | ex 412 | . . . . . . 7
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → (ω ⊆ dom OrdIso(𝑅, 𝐴) → ∃𝑦 ∈ ω ∀𝑧 ∈ ω ¬ 𝑧◡ E
𝑦)) | 
| 47 | 26, 46 | biimtrrid 243 | . . . . . 6
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → (¬ dom OrdIso(𝑅, 𝐴) ∈ ω → ∃𝑦 ∈ ω ∀𝑧 ∈ ω ¬ 𝑧◡ E 𝑦)) | 
| 48 | 21, 47 | mt3i 149 | . . . . 5
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → dom OrdIso(𝑅, 𝐴) ∈ ω) | 
| 49 |  | ssid 4006 | . . . . 5
⊢ dom
OrdIso(𝑅, 𝐴) ⊆ dom OrdIso(𝑅, 𝐴) | 
| 50 |  | ssnnfi 9209 | . . . . 5
⊢ ((dom
OrdIso(𝑅, 𝐴) ∈ ω ∧ dom OrdIso(𝑅, 𝐴) ⊆ dom OrdIso(𝑅, 𝐴)) → dom OrdIso(𝑅, 𝐴) ∈ Fin) | 
| 51 | 48, 49, 50 | sylancl 586 | . . . 4
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → dom OrdIso(𝑅, 𝐴) ∈ Fin) | 
| 52 |  | simpl 482 | . . . . . 6
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → 𝑅 We 𝐴) | 
| 53 | 23 | oien 9578 | . . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝑅 We 𝐴) → dom OrdIso(𝑅, 𝐴) ≈ 𝐴) | 
| 54 | 27, 52, 53 | sylancr 587 | . . . . 5
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → dom OrdIso(𝑅, 𝐴) ≈ 𝐴) | 
| 55 |  | enfi 9227 | . . . . 5
⊢ (dom
OrdIso(𝑅, 𝐴) ≈ 𝐴 → (dom OrdIso(𝑅, 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin)) | 
| 56 | 54, 55 | syl 17 | . . . 4
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → (dom OrdIso(𝑅, 𝐴) ∈ Fin ↔ 𝐴 ∈ Fin)) | 
| 57 | 51, 56 | mpbid 232 | . . 3
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → 𝐴 ∈ Fin) | 
| 58 | 7, 57 | jca 511 | . 2
⊢ ((𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴) → (𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin)) | 
| 59 | 5, 58 | impbii 209 | 1
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ↔ (𝑅 We 𝐴 ∧ ◡𝑅 We 𝐴)) |