| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq2 2829 | . . . 4
⊢ (𝑥 = ∅ → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ ∅)) | 
| 2 |  | fveq2 6905 | . . . . 5
⊢ (𝑥 = ∅ →
(𝑅1‘𝑥) =
(𝑅1‘∅)) | 
| 3 | 2 | breq2d 5154 | . . . 4
⊢ (𝑥 = ∅ →
((𝑅1‘𝐵) ≺ (𝑅1‘𝑥) ↔
(𝑅1‘𝐵) ≺
(𝑅1‘∅))) | 
| 4 | 1, 3 | imbi12d 344 | . . 3
⊢ (𝑥 = ∅ → ((𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)) ↔ (𝐵 ∈ ∅ →
(𝑅1‘𝐵) ≺
(𝑅1‘∅)))) | 
| 5 |  | eleq2 2829 | . . . 4
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ 𝑦)) | 
| 6 |  | fveq2 6905 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) | 
| 7 | 6 | breq2d 5154 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝑅1‘𝐵) ≺
(𝑅1‘𝑥) ↔ (𝑅1‘𝐵) ≺
(𝑅1‘𝑦))) | 
| 8 | 5, 7 | imbi12d 344 | . . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)) ↔ (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)))) | 
| 9 |  | eleq2 2829 | . . . 4
⊢ (𝑥 = suc 𝑦 → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ suc 𝑦)) | 
| 10 |  | fveq2 6905 | . . . . 5
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) | 
| 11 | 10 | breq2d 5154 | . . . 4
⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝐵) ≺
(𝑅1‘𝑥) ↔ (𝑅1‘𝐵) ≺
(𝑅1‘suc 𝑦))) | 
| 12 | 9, 11 | imbi12d 344 | . . 3
⊢ (𝑥 = suc 𝑦 → ((𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)) ↔ (𝐵 ∈ suc 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘suc 𝑦)))) | 
| 13 |  | eleq2 2829 | . . . 4
⊢ (𝑥 = 𝐴 → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ 𝐴)) | 
| 14 |  | fveq2 6905 | . . . . 5
⊢ (𝑥 = 𝐴 → (𝑅1‘𝑥) =
(𝑅1‘𝐴)) | 
| 15 | 14 | breq2d 5154 | . . . 4
⊢ (𝑥 = 𝐴 → ((𝑅1‘𝐵) ≺
(𝑅1‘𝑥) ↔ (𝑅1‘𝐵) ≺
(𝑅1‘𝐴))) | 
| 16 | 13, 15 | imbi12d 344 | . . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)) ↔ (𝐵 ∈ 𝐴 → (𝑅1‘𝐵) ≺
(𝑅1‘𝐴)))) | 
| 17 |  | noel 4337 | . . . 4
⊢  ¬
𝐵 ∈
∅ | 
| 18 | 17 | pm2.21i 119 | . . 3
⊢ (𝐵 ∈ ∅ →
(𝑅1‘𝐵) ≺
(𝑅1‘∅)) | 
| 19 |  | elsuci 6450 | . . . . 5
⊢ (𝐵 ∈ suc 𝑦 → (𝐵 ∈ 𝑦 ∨ 𝐵 = 𝑦)) | 
| 20 |  | sdomtr 9156 | . . . . . . . . 9
⊢
(((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) ∧
(𝑅1‘𝑦) ≺ (𝑅1‘suc
𝑦)) →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)) | 
| 21 | 20 | expcom 413 | . . . . . . . 8
⊢
((𝑅1‘𝑦) ≺ (𝑅1‘suc
𝑦) →
((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦))) | 
| 22 |  | fvex 6918 | . . . . . . . . . 10
⊢
(𝑅1‘𝑦) ∈ V | 
| 23 | 22 | canth2 9171 | . . . . . . . . 9
⊢
(𝑅1‘𝑦) ≺ 𝒫
(𝑅1‘𝑦) | 
| 24 |  | r1suc 9811 | . . . . . . . . 9
⊢ (𝑦 ∈ On →
(𝑅1‘suc 𝑦) = 𝒫
(𝑅1‘𝑦)) | 
| 25 | 23, 24 | breqtrrid 5180 | . . . . . . . 8
⊢ (𝑦 ∈ On →
(𝑅1‘𝑦) ≺ (𝑅1‘suc
𝑦)) | 
| 26 | 21, 25 | syl11 33 | . . . . . . 7
⊢
((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦))) | 
| 27 | 26 | imim2i 16 | . . . . . 6
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ 𝑦 → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)))) | 
| 28 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝐵 = 𝑦 → (𝑅1‘𝐵) =
(𝑅1‘𝑦)) | 
| 29 | 28 | breq1d 5152 | . . . . . . . 8
⊢ (𝐵 = 𝑦 → ((𝑅1‘𝐵) ≺
(𝑅1‘suc 𝑦) ↔ (𝑅1‘𝑦) ≺
(𝑅1‘suc 𝑦))) | 
| 30 | 25, 29 | imbitrrid 246 | . . . . . . 7
⊢ (𝐵 = 𝑦 → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦))) | 
| 31 | 30 | a1i 11 | . . . . . 6
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 = 𝑦 → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)))) | 
| 32 | 27, 31 | jaod 859 | . . . . 5
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → ((𝐵 ∈ 𝑦 ∨ 𝐵 = 𝑦) → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)))) | 
| 33 | 19, 32 | syl5 34 | . . . 4
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ suc 𝑦 → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)))) | 
| 34 | 33 | com3r 87 | . . 3
⊢ (𝑦 ∈ On → ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ suc 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘suc 𝑦)))) | 
| 35 |  | limuni 6444 | . . . . . . 7
⊢ (Lim
𝑥 → 𝑥 = ∪ 𝑥) | 
| 36 | 35 | eleq2d 2826 | . . . . . 6
⊢ (Lim
𝑥 → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ ∪ 𝑥)) | 
| 37 |  | eluni2 4910 | . . . . . 6
⊢ (𝐵 ∈ ∪ 𝑥
↔ ∃𝑦 ∈
𝑥 𝐵 ∈ 𝑦) | 
| 38 | 36, 37 | bitrdi 287 | . . . . 5
⊢ (Lim
𝑥 → (𝐵 ∈ 𝑥 ↔ ∃𝑦 ∈ 𝑥 𝐵 ∈ 𝑦)) | 
| 39 |  | r19.29 3113 | . . . . . . 7
⊢
((∀𝑦 ∈
𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ ∃𝑦 ∈ 𝑥 𝐵 ∈ 𝑦) → ∃𝑦 ∈ 𝑥 ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦)) | 
| 40 |  | fvex 6918 | . . . . . . . . . 10
⊢
(𝑅1‘𝑥) ∈ V | 
| 41 |  | ssiun2 5046 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ⊆ ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) | 
| 42 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 43 |  | r1lim 9813 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) →
(𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) | 
| 44 | 42, 43 | mpan 690 | . . . . . . . . . . . 12
⊢ (Lim
𝑥 →
(𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) | 
| 45 | 44 | sseq2d 4015 | . . . . . . . . . . 11
⊢ (Lim
𝑥 →
((𝑅1‘𝑦) ⊆ (𝑅1‘𝑥) ↔
(𝑅1‘𝑦) ⊆ ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦))) | 
| 46 | 41, 45 | imbitrrid 246 | . . . . . . . . . 10
⊢ (Lim
𝑥 → (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ⊆
(𝑅1‘𝑥))) | 
| 47 |  | ssdomg 9041 | . . . . . . . . . 10
⊢
((𝑅1‘𝑥) ∈ V →
((𝑅1‘𝑦) ⊆ (𝑅1‘𝑥) →
(𝑅1‘𝑦) ≼ (𝑅1‘𝑥))) | 
| 48 | 40, 46, 47 | mpsylsyld 69 | . . . . . . . . 9
⊢ (Lim
𝑥 → (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ≼
(𝑅1‘𝑥))) | 
| 49 |  | id 22 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦))) | 
| 50 | 49 | imp 406 | . . . . . . . . . 10
⊢ (((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) | 
| 51 |  | sdomdomtr 9151 | . . . . . . . . . . 11
⊢
(((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) ∧
(𝑅1‘𝑦) ≼ (𝑅1‘𝑥)) →
(𝑅1‘𝐵) ≺ (𝑅1‘𝑥)) | 
| 52 | 51 | expcom 413 | . . . . . . . . . 10
⊢
((𝑅1‘𝑦) ≼ (𝑅1‘𝑥) →
((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) →
(𝑅1‘𝐵) ≺ (𝑅1‘𝑥))) | 
| 53 | 50, 52 | syl5 34 | . . . . . . . . 9
⊢
((𝑅1‘𝑦) ≼ (𝑅1‘𝑥) → (((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥))) | 
| 54 | 48, 53 | syl6 35 | . . . . . . . 8
⊢ (Lim
𝑥 → (𝑦 ∈ 𝑥 → (((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)))) | 
| 55 | 54 | rexlimdv 3152 | . . . . . . 7
⊢ (Lim
𝑥 → (∃𝑦 ∈ 𝑥 ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥))) | 
| 56 | 39, 55 | syl5 34 | . . . . . 6
⊢ (Lim
𝑥 → ((∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ ∃𝑦 ∈ 𝑥 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥))) | 
| 57 | 56 | expcomd 416 | . . . . 5
⊢ (Lim
𝑥 → (∃𝑦 ∈ 𝑥 𝐵 ∈ 𝑦 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)))) | 
| 58 | 38, 57 | sylbid 240 | . . . 4
⊢ (Lim
𝑥 → (𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)))) | 
| 59 | 58 | com23 86 | . . 3
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)))) | 
| 60 | 4, 8, 12, 16, 18, 34, 59 | tfinds 7882 | . 2
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → (𝑅1‘𝐵) ≺
(𝑅1‘𝐴))) | 
| 61 | 60 | imp 406 | 1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → (𝑅1‘𝐵) ≺
(𝑅1‘𝐴)) |