Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = suc 𝐴 → (𝐶 ↑𝑜 𝑥) = (𝐶 ↑𝑜 suc 𝐴)) |
2 | 1 | eleq2d 2687 |
. . . 4
⊢ (𝑥 = suc 𝐴 → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥) ↔ (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴))) |
3 | 2 | imbi2d 330 |
. . 3
⊢ (𝑥 = suc 𝐴 → ((𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥)) ↔ (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴)))) |
4 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐶 ↑𝑜 𝑥) = (𝐶 ↑𝑜 𝑦)) |
5 | 4 | eleq2d 2687 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥) ↔ (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦))) |
6 | 5 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥)) ↔ (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)))) |
7 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐶 ↑𝑜 𝑥) = (𝐶 ↑𝑜 suc 𝑦)) |
8 | 7 | eleq2d 2687 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥) ↔ (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝑦))) |
9 | 8 | imbi2d 330 |
. . 3
⊢ (𝑥 = suc 𝑦 → ((𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥)) ↔ (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝑦)))) |
10 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐶 ↑𝑜 𝑥) = (𝐶 ↑𝑜 𝐵)) |
11 | 10 | eleq2d 2687 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥) ↔ (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵))) |
12 | 11 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥)) ↔ (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵)))) |
13 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝐶 ∈ (On ∖
2𝑜) → 𝐶 ∈ On) |
14 | | oecl 7617 |
. . . . . . . 8
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ↑𝑜
𝐴) ∈
On) |
15 | 13, 14 | sylan 488 |
. . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → (𝐶 ↑𝑜 𝐴) ∈ On) |
16 | | om1 7622 |
. . . . . . 7
⊢ ((𝐶 ↑𝑜
𝐴) ∈ On → ((𝐶 ↑𝑜
𝐴)
·𝑜 1𝑜) = (𝐶 ↑𝑜 𝐴)) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → ((𝐶 ↑𝑜 𝐴) ·𝑜
1𝑜) = (𝐶
↑𝑜 𝐴)) |
18 | | ondif2 7582 |
. . . . . . . . 9
⊢ (𝐶 ∈ (On ∖
2𝑜) ↔ (𝐶 ∈ On ∧ 1𝑜
∈ 𝐶)) |
19 | 18 | simprbi 480 |
. . . . . . . 8
⊢ (𝐶 ∈ (On ∖
2𝑜) → 1𝑜 ∈ 𝐶) |
20 | 19 | adantr 481 |
. . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → 1𝑜
∈ 𝐶) |
21 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → 𝐶 ∈ On) |
22 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → 𝐴 ∈ On) |
23 | | dif20el 7585 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (On ∖
2𝑜) → ∅ ∈ 𝐶) |
24 | 23 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → ∅ ∈ 𝐶) |
25 | | oen0 7666 |
. . . . . . . . 9
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐶) → ∅ ∈
(𝐶
↑𝑜 𝐴)) |
26 | 21, 22, 24, 25 | syl21anc 1325 |
. . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → ∅ ∈ (𝐶 ↑𝑜
𝐴)) |
27 | | omordi 7646 |
. . . . . . . 8
⊢ (((𝐶 ∈ On ∧ (𝐶 ↑𝑜
𝐴) ∈ On) ∧ ∅
∈ (𝐶
↑𝑜 𝐴)) → (1𝑜 ∈
𝐶 → ((𝐶 ↑𝑜
𝐴)
·𝑜 1𝑜) ∈ ((𝐶 ↑𝑜 𝐴) ·𝑜
𝐶))) |
28 | 21, 15, 26, 27 | syl21anc 1325 |
. . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → (1𝑜
∈ 𝐶 → ((𝐶 ↑𝑜
𝐴)
·𝑜 1𝑜) ∈ ((𝐶 ↑𝑜 𝐴) ·𝑜
𝐶))) |
29 | 20, 28 | mpd 15 |
. . . . . 6
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → ((𝐶 ↑𝑜 𝐴) ·𝑜
1𝑜) ∈ ((𝐶 ↑𝑜 𝐴) ·𝑜
𝐶)) |
30 | 17, 29 | eqeltrrd 2702 |
. . . . 5
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → (𝐶 ↑𝑜 𝐴) ∈ ((𝐶 ↑𝑜 𝐴) ·𝑜
𝐶)) |
31 | | oesuc 7607 |
. . . . . 6
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ↑𝑜 suc
𝐴) = ((𝐶 ↑𝑜 𝐴) ·𝑜
𝐶)) |
32 | 13, 31 | sylan 488 |
. . . . 5
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → (𝐶 ↑𝑜 suc 𝐴) = ((𝐶 ↑𝑜 𝐴) ·𝑜
𝐶)) |
33 | 30, 32 | eleqtrrd 2704 |
. . . 4
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝐴 ∈ On) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴)) |
34 | 33 | expcom 451 |
. . 3
⊢ (𝐴 ∈ On → (𝐶 ∈ (On ∖
2𝑜) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴))) |
35 | | oecl 7617 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ↑𝑜
𝑦) ∈
On) |
36 | 13, 35 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝐶 ↑𝑜 𝑦) ∈ On) |
37 | | om1 7622 |
. . . . . . . . . 10
⊢ ((𝐶 ↑𝑜
𝑦) ∈ On → ((𝐶 ↑𝑜
𝑦)
·𝑜 1𝑜) = (𝐶 ↑𝑜 𝑦)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → ((𝐶 ↑𝑜 𝑦) ·𝑜
1𝑜) = (𝐶
↑𝑜 𝑦)) |
39 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → 1𝑜
∈ 𝐶) |
40 | 13 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → 𝐶 ∈ On) |
41 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → 𝑦 ∈ On) |
42 | 23 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → ∅ ∈ 𝐶) |
43 | | oen0 7666 |
. . . . . . . . . . . 12
⊢ (((𝐶 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈
𝐶) → ∅ ∈
(𝐶
↑𝑜 𝑦)) |
44 | 40, 41, 42, 43 | syl21anc 1325 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → ∅ ∈ (𝐶 ↑𝑜
𝑦)) |
45 | | omordi 7646 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ On ∧ (𝐶 ↑𝑜
𝑦) ∈ On) ∧ ∅
∈ (𝐶
↑𝑜 𝑦)) → (1𝑜 ∈ 𝐶 → ((𝐶 ↑𝑜 𝑦) ·𝑜
1𝑜) ∈ ((𝐶 ↑𝑜 𝑦) ·𝑜
𝐶))) |
46 | 40, 36, 44, 45 | syl21anc 1325 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (1𝑜
∈ 𝐶 → ((𝐶 ↑𝑜
𝑦)
·𝑜 1𝑜) ∈ ((𝐶 ↑𝑜 𝑦) ·𝑜
𝐶))) |
47 | 39, 46 | mpd 15 |
. . . . . . . . 9
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → ((𝐶 ↑𝑜 𝑦) ·𝑜
1𝑜) ∈ ((𝐶 ↑𝑜 𝑦) ·𝑜
𝐶)) |
48 | 38, 47 | eqeltrrd 2702 |
. . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝐶 ↑𝑜 𝑦) ∈ ((𝐶 ↑𝑜 𝑦) ·𝑜
𝐶)) |
49 | | oesuc 7607 |
. . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ↑𝑜 suc
𝑦) = ((𝐶 ↑𝑜 𝑦) ·𝑜
𝐶)) |
50 | 13, 49 | sylan 488 |
. . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝐶 ↑𝑜 suc 𝑦) = ((𝐶 ↑𝑜 𝑦) ·𝑜
𝐶)) |
51 | 48, 50 | eleqtrrd 2704 |
. . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝐶 ↑𝑜 𝑦) ∈ (𝐶 ↑𝑜 suc 𝑦)) |
52 | | suceloni 7013 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
53 | | oecl 7617 |
. . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ suc 𝑦 ∈ On) → (𝐶 ↑𝑜 suc
𝑦) ∈
On) |
54 | 13, 52, 53 | syl2an 494 |
. . . . . . . 8
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (𝐶 ↑𝑜 suc 𝑦) ∈ On) |
55 | | ontr1 5771 |
. . . . . . . 8
⊢ ((𝐶 ↑𝑜 suc
𝑦) ∈ On →
(((𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦) ∧ (𝐶 ↑𝑜 𝑦) ∈ (𝐶 ↑𝑜 suc 𝑦)) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝑦))) |
56 | 54, 55 | syl 17 |
. . . . . . 7
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → (((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦) ∧ (𝐶 ↑𝑜 𝑦) ∈ (𝐶 ↑𝑜 suc 𝑦)) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝑦))) |
57 | 51, 56 | mpan2d 710 |
. . . . . 6
⊢ ((𝐶 ∈ (On ∖
2𝑜) ∧ 𝑦 ∈ On) → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝑦))) |
58 | 57 | expcom 451 |
. . . . 5
⊢ (𝑦 ∈ On → (𝐶 ∈ (On ∖
2𝑜) → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝑦)))) |
59 | 58 | adantr 481 |
. . . 4
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ 𝑦) → (𝐶 ∈ (On ∖ 2𝑜)
→ ((𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝑦)))) |
60 | 59 | a2d 29 |
. . 3
⊢ ((𝑦 ∈ On ∧ 𝐴 ∈ 𝑦) → ((𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝑦)))) |
61 | | bi2.04 376 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑦 → (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦))) ↔ (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)))) |
62 | 61 | ralbii 2980 |
. . . . 5
⊢
(∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦))) ↔ ∀𝑦 ∈ 𝑥 (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)))) |
63 | | r19.21v 2960 |
. . . . 5
⊢
(∀𝑦 ∈
𝑥 (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦))) ↔ (𝐶 ∈ (On ∖ 2𝑜)
→ ∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)))) |
64 | 62, 63 | bitri 264 |
. . . 4
⊢
(∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦))) ↔ (𝐶 ∈ (On ∖ 2𝑜)
→ ∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)))) |
65 | | limsuc 7049 |
. . . . . . . . . 10
⊢ (Lim
𝑥 → (𝐴 ∈ 𝑥 ↔ suc 𝐴 ∈ 𝑥)) |
66 | 65 | biimpa 501 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → suc 𝐴 ∈ 𝑥) |
67 | | elex 3212 |
. . . . . . . . . . . . 13
⊢ (suc
𝐴 ∈ 𝑥 → suc 𝐴 ∈ V) |
68 | | sucexb 7009 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) |
69 | | sucidg 5803 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) |
70 | 68, 69 | sylbir 225 |
. . . . . . . . . . . . 13
⊢ (suc
𝐴 ∈ V → 𝐴 ∈ suc 𝐴) |
71 | 67, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ (suc
𝐴 ∈ 𝑥 → 𝐴 ∈ suc 𝐴) |
72 | | eleq2 2690 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = suc 𝐴 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ suc 𝐴)) |
73 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = suc 𝐴 → (𝐶 ↑𝑜 𝑦) = (𝐶 ↑𝑜 suc 𝐴)) |
74 | 73 | eleq2d 2687 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = suc 𝐴 → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦) ↔ (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴))) |
75 | 72, 74 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ (𝑦 = suc 𝐴 → ((𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) ↔ (𝐴 ∈ suc 𝐴 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴)))) |
76 | 75 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ (suc
𝐴 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (𝐴 ∈ suc 𝐴 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴)))) |
77 | 71, 76 | mpid 44 |
. . . . . . . . . . 11
⊢ (suc
𝐴 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴))) |
78 | 77 | anc2li 580 |
. . . . . . . . . 10
⊢ (suc
𝐴 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (suc 𝐴 ∈ 𝑥 ∧ (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴)))) |
79 | 73 | eliuni 4526 |
. . . . . . . . . 10
⊢ ((suc
𝐴 ∈ 𝑥 ∧ (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 suc 𝐴)) → (𝐶 ↑𝑜 𝐴) ∈ ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦)) |
80 | 78, 79 | syl6 35 |
. . . . . . . . 9
⊢ (suc
𝐴 ∈ 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (𝐶 ↑𝑜 𝐴) ∈ ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦))) |
81 | 66, 80 | syl 17 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (𝐶 ↑𝑜 𝐴) ∈ ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦))) |
82 | 81 | adantr 481 |
. . . . . . 7
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) ∧ 𝐶 ∈ (On ∖ 2𝑜))
→ (∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (𝐶 ↑𝑜 𝐴) ∈ ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦))) |
83 | 13 | adantl 482 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ (On ∖ 2𝑜))
→ 𝐶 ∈
On) |
84 | | simpl 473 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ (On ∖ 2𝑜))
→ Lim 𝑥) |
85 | 23 | adantl 482 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ (On ∖ 2𝑜))
→ ∅ ∈ 𝐶) |
86 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
87 | | oelim 7614 |
. . . . . . . . . . 11
⊢ (((𝐶 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐶) → (𝐶 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦)) |
88 | 86, 87 | mpanlr1 722 |
. . . . . . . . . 10
⊢ (((𝐶 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐶) → (𝐶 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦)) |
89 | 83, 84, 85, 88 | syl21anc 1325 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ 𝐶 ∈ (On ∖ 2𝑜))
→ (𝐶
↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦)) |
90 | 89 | adantlr 751 |
. . . . . . . 8
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) ∧ 𝐶 ∈ (On ∖ 2𝑜))
→ (𝐶
↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦)) |
91 | 90 | eleq2d 2687 |
. . . . . . 7
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) ∧ 𝐶 ∈ (On ∖ 2𝑜))
→ ((𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥) ↔ (𝐶 ↑𝑜 𝐴) ∈ ∪ 𝑦 ∈ 𝑥 (𝐶 ↑𝑜 𝑦))) |
92 | 82, 91 | sylibrd 249 |
. . . . . 6
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) ∧ 𝐶 ∈ (On ∖ 2𝑜))
→ (∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥))) |
93 | 92 | ex 450 |
. . . . 5
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → (𝐶 ∈ (On ∖ 2𝑜)
→ (∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦)) → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥)))) |
94 | 93 | a2d 29 |
. . . 4
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → ((𝐶 ∈ (On ∖ 2𝑜)
→ ∀𝑦 ∈
𝑥 (𝐴 ∈ 𝑦 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦))) → (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥)))) |
95 | 64, 94 | syl5bi 232 |
. . 3
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ 𝑥) → (∀𝑦 ∈ 𝑥 (𝐴 ∈ 𝑦 → (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑦))) → (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝑥)))) |
96 | 3, 6, 9, 12, 34, 60, 95 | tfindsg2 7061 |
. 2
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐶 ∈ (On ∖ 2𝑜)
→ (𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵))) |
97 | 96 | impancom 456 |
1
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐴 ∈ 𝐵 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵))) |