Step | Hyp | Ref
| Expression |
1 | | eleq2 2677 |
. . . 4
⊢ (𝑥 = ∅ → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ ∅)) |
2 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = ∅ →
(𝑅1‘𝑥) =
(𝑅1‘∅)) |
3 | 2 | breq2d 4595 |
. . . 4
⊢ (𝑥 = ∅ →
((𝑅1‘𝐵) ≺ (𝑅1‘𝑥) ↔
(𝑅1‘𝐵) ≺
(𝑅1‘∅))) |
4 | 1, 3 | imbi12d 333 |
. . 3
⊢ (𝑥 = ∅ → ((𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)) ↔ (𝐵 ∈ ∅ →
(𝑅1‘𝐵) ≺
(𝑅1‘∅)))) |
5 | | eleq2 2677 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ 𝑦)) |
6 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘𝑦)) |
7 | 6 | breq2d 4595 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑅1‘𝐵) ≺
(𝑅1‘𝑥) ↔ (𝑅1‘𝐵) ≺
(𝑅1‘𝑦))) |
8 | 5, 7 | imbi12d 333 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)) ↔ (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)))) |
9 | | eleq2 2677 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ suc 𝑦)) |
10 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝑅1‘𝑥) =
(𝑅1‘suc 𝑦)) |
11 | 10 | breq2d 4595 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝑅1‘𝐵) ≺
(𝑅1‘𝑥) ↔ (𝑅1‘𝐵) ≺
(𝑅1‘suc 𝑦))) |
12 | 9, 11 | imbi12d 333 |
. . 3
⊢ (𝑥 = suc 𝑦 → ((𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)) ↔ (𝐵 ∈ suc 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘suc 𝑦)))) |
13 | | eleq2 2677 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ 𝐴)) |
14 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑅1‘𝑥) =
(𝑅1‘𝐴)) |
15 | 14 | breq2d 4595 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑅1‘𝐵) ≺
(𝑅1‘𝑥) ↔ (𝑅1‘𝐵) ≺
(𝑅1‘𝐴))) |
16 | 13, 15 | imbi12d 333 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)) ↔ (𝐵 ∈ 𝐴 → (𝑅1‘𝐵) ≺
(𝑅1‘𝐴)))) |
17 | | noel 3878 |
. . . 4
⊢ ¬
𝐵 ∈
∅ |
18 | 17 | pm2.21i 115 |
. . 3
⊢ (𝐵 ∈ ∅ →
(𝑅1‘𝐵) ≺
(𝑅1‘∅)) |
19 | | elsuci 5708 |
. . . . 5
⊢ (𝐵 ∈ suc 𝑦 → (𝐵 ∈ 𝑦 ∨ 𝐵 = 𝑦)) |
20 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(𝑅1‘𝑦) ∈ V |
21 | 20 | canth2 7998 |
. . . . . . . . . 10
⊢
(𝑅1‘𝑦) ≺ 𝒫
(𝑅1‘𝑦) |
22 | | r1suc 8516 |
. . . . . . . . . 10
⊢ (𝑦 ∈ On →
(𝑅1‘suc 𝑦) = 𝒫
(𝑅1‘𝑦)) |
23 | 21, 22 | syl5breqr 4621 |
. . . . . . . . 9
⊢ (𝑦 ∈ On →
(𝑅1‘𝑦) ≺ (𝑅1‘suc
𝑦)) |
24 | | sdomtr 7983 |
. . . . . . . . . 10
⊢
(((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) ∧
(𝑅1‘𝑦) ≺ (𝑅1‘suc
𝑦)) →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)) |
25 | 24 | expcom 450 |
. . . . . . . . 9
⊢
((𝑅1‘𝑦) ≺ (𝑅1‘suc
𝑦) →
((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦))) |
26 | 23, 25 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ On →
((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦))) |
27 | 26 | com12 32 |
. . . . . . 7
⊢
((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦))) |
28 | 27 | imim2i 16 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ 𝑦 → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)))) |
29 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝐵 = 𝑦 → (𝑅1‘𝐵) =
(𝑅1‘𝑦)) |
30 | 29 | breq1d 4593 |
. . . . . . . 8
⊢ (𝐵 = 𝑦 → ((𝑅1‘𝐵) ≺
(𝑅1‘suc 𝑦) ↔ (𝑅1‘𝑦) ≺
(𝑅1‘suc 𝑦))) |
31 | 23, 30 | syl5ibr 235 |
. . . . . . 7
⊢ (𝐵 = 𝑦 → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦))) |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 = 𝑦 → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)))) |
33 | 28, 32 | jaod 394 |
. . . . 5
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → ((𝐵 ∈ 𝑦 ∨ 𝐵 = 𝑦) → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)))) |
34 | 19, 33 | syl5 33 |
. . . 4
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ suc 𝑦 → (𝑦 ∈ On →
(𝑅1‘𝐵) ≺ (𝑅1‘suc
𝑦)))) |
35 | 34 | com3r 85 |
. . 3
⊢ (𝑦 ∈ On → ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ suc 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘suc 𝑦)))) |
36 | | limuni 5702 |
. . . . . . 7
⊢ (Lim
𝑥 → 𝑥 = ∪ 𝑥) |
37 | 36 | eleq2d 2673 |
. . . . . 6
⊢ (Lim
𝑥 → (𝐵 ∈ 𝑥 ↔ 𝐵 ∈ ∪ 𝑥)) |
38 | | eluni2 4376 |
. . . . . 6
⊢ (𝐵 ∈ ∪ 𝑥
↔ ∃𝑦 ∈
𝑥 𝐵 ∈ 𝑦) |
39 | 37, 38 | syl6bb 275 |
. . . . 5
⊢ (Lim
𝑥 → (𝐵 ∈ 𝑥 ↔ ∃𝑦 ∈ 𝑥 𝐵 ∈ 𝑦)) |
40 | | r19.29 3054 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ ∃𝑦 ∈ 𝑥 𝐵 ∈ 𝑦) → ∃𝑦 ∈ 𝑥 ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦)) |
41 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(𝑅1‘𝑥) ∈ V |
42 | 41 | a1i 11 |
. . . . . . . . . 10
⊢ (Lim
𝑥 →
(𝑅1‘𝑥) ∈ V) |
43 | | ssiun2 4499 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ⊆ ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) |
44 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
45 | | r1lim 8518 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) →
(𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) |
46 | 44, 45 | mpan 702 |
. . . . . . . . . . . 12
⊢ (Lim
𝑥 →
(𝑅1‘𝑥) = ∪ 𝑦 ∈ 𝑥 (𝑅1‘𝑦)) |
47 | 46 | sseq2d 3596 |
. . . . . . . . . . 11
⊢ (Lim
𝑥 →
((𝑅1‘𝑦) ⊆ (𝑅1‘𝑥) ↔
(𝑅1‘𝑦) ⊆ ∪
𝑦 ∈ 𝑥 (𝑅1‘𝑦))) |
48 | 43, 47 | syl5ibr 235 |
. . . . . . . . . 10
⊢ (Lim
𝑥 → (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ⊆
(𝑅1‘𝑥))) |
49 | | ssdomg 7887 |
. . . . . . . . . 10
⊢
((𝑅1‘𝑥) ∈ V →
((𝑅1‘𝑦) ⊆ (𝑅1‘𝑥) →
(𝑅1‘𝑦) ≼ (𝑅1‘𝑥))) |
50 | 42, 48, 49 | sylsyld 59 |
. . . . . . . . 9
⊢ (Lim
𝑥 → (𝑦 ∈ 𝑥 → (𝑅1‘𝑦) ≼
(𝑅1‘𝑥))) |
51 | | id 22 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦))) |
52 | 51 | imp 444 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) |
53 | | sdomdomtr 7978 |
. . . . . . . . . . 11
⊢
(((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) ∧
(𝑅1‘𝑦) ≼ (𝑅1‘𝑥)) →
(𝑅1‘𝐵) ≺ (𝑅1‘𝑥)) |
54 | 53 | expcom 450 |
. . . . . . . . . 10
⊢
((𝑅1‘𝑦) ≼ (𝑅1‘𝑥) →
((𝑅1‘𝐵) ≺ (𝑅1‘𝑦) →
(𝑅1‘𝐵) ≺ (𝑅1‘𝑥))) |
55 | 52, 54 | syl5 33 |
. . . . . . . . 9
⊢
((𝑅1‘𝑦) ≼ (𝑅1‘𝑥) → (((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥))) |
56 | 50, 55 | syl6 34 |
. . . . . . . 8
⊢ (Lim
𝑥 → (𝑦 ∈ 𝑥 → (((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)))) |
57 | 56 | rexlimdv 3012 |
. . . . . . 7
⊢ (Lim
𝑥 → (∃𝑦 ∈ 𝑥 ((𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥))) |
58 | 40, 57 | syl5 33 |
. . . . . 6
⊢ (Lim
𝑥 → ((∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) ∧ ∃𝑦 ∈ 𝑥 𝐵 ∈ 𝑦) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥))) |
59 | 58 | expcomd 453 |
. . . . 5
⊢ (Lim
𝑥 → (∃𝑦 ∈ 𝑥 𝐵 ∈ 𝑦 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)))) |
60 | 39, 59 | sylbid 229 |
. . . 4
⊢ (Lim
𝑥 → (𝐵 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)))) |
61 | 60 | com23 84 |
. . 3
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (𝐵 ∈ 𝑦 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑦)) → (𝐵 ∈ 𝑥 → (𝑅1‘𝐵) ≺
(𝑅1‘𝑥)))) |
62 | 4, 8, 12, 16, 18, 35, 61 | tfinds 6951 |
. 2
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → (𝑅1‘𝐵) ≺
(𝑅1‘𝐴))) |
63 | 62 | imp 444 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → (𝑅1‘𝐵) ≺
(𝑅1‘𝐴)) |