Step | Hyp | Ref
| Expression |
1 | | nfsbc1v 3705 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥[∅ / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) |
2 | | 0ex 5185 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
3 | | rzal 4405 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → ∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) |
4 | | sbceq1a 3696 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ [∅ / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) |
5 | 3, 4 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ →
[∅ / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) |
6 | 1, 2, 5 | vtoclef 3491 |
. . . . . . . . . . 11
⊢
[∅ / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) |
7 | | vex 3404 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
8 | 7 | elsuc 6251 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ suc 𝑥 ↔ (𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥)) |
9 | | ssun1 4072 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(rec(𝐹, 𝐴)‘𝑥) ⊆ ((rec(𝐹, 𝐴)‘𝑥) ∪ ⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵) |
10 | | fvex 6699 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(rec(𝐹, 𝐴)‘𝑥) ∈ V |
11 | | rdgssun.2 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐵 ∈ V |
12 | 11 | csbex 5189 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵 ∈ V |
13 | 10, 12 | unex 7499 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((rec(𝐹, 𝐴)‘𝑥) ∪ ⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵) ∈ V |
14 | | nfcv 2900 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤𝐴 |
15 | | nfcv 2900 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤𝑥 |
16 | | rdgssun.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐹 = (𝑤 ∈ V ↦ (𝑤 ∪ 𝐵)) |
17 | | nfmpt1 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑤(𝑤 ∈ V ↦ (𝑤 ∪ 𝐵)) |
18 | 16, 17 | nfcxfr 2898 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑤𝐹 |
19 | 18, 14 | nfrdg 8091 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑤rec(𝐹, 𝐴) |
20 | 19, 15 | nffv 6696 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑤(rec(𝐹, 𝐴)‘𝑥) |
21 | 20 | nfcsb1 3823 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑤⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵 |
22 | 20, 21 | nfun 4065 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤((rec(𝐹, 𝐴)‘𝑥) ∪ ⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵) |
23 | | rdgeq1 8088 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 = (𝑤 ∈ V ↦ (𝑤 ∪ 𝐵)) → rec(𝐹, 𝐴) = rec((𝑤 ∈ V ↦ (𝑤 ∪ 𝐵)), 𝐴)) |
24 | 16, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ rec(𝐹, 𝐴) = rec((𝑤 ∈ V ↦ (𝑤 ∪ 𝐵)), 𝐴) |
25 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = (rec(𝐹, 𝐴)‘𝑥) → 𝑤 = (rec(𝐹, 𝐴)‘𝑥)) |
26 | | csbeq1a 3814 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = (rec(𝐹, 𝐴)‘𝑥) → 𝐵 = ⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵) |
27 | 25, 26 | uneq12d 4064 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = (rec(𝐹, 𝐴)‘𝑥) → (𝑤 ∪ 𝐵) = ((rec(𝐹, 𝐴)‘𝑥) ∪ ⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵)) |
28 | 14, 15, 22, 24, 27 | rdgsucmptf 8105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ ((rec(𝐹, 𝐴)‘𝑥) ∪ ⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵) ∈ V) → (rec(𝐹, 𝐴)‘suc 𝑥) = ((rec(𝐹, 𝐴)‘𝑥) ∪ ⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵)) |
29 | 13, 28 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ On → (rec(𝐹, 𝐴)‘suc 𝑥) = ((rec(𝐹, 𝐴)‘𝑥) ∪ ⦋(rec(𝐹, 𝐴)‘𝑥) / 𝑤⦌𝐵)) |
30 | 9, 29 | sseqtrrid 3940 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ On → (rec(𝐹, 𝐴)‘𝑥) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)) |
31 | | sstr2 3894 |
. . . . . . . . . . . . . . . . . . 19
⊢
((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → ((rec(𝐹, 𝐴)‘𝑥) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥) → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
32 | 30, 31 | syl5com 31 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ On → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
33 | 32 | imim2d 57 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) → (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))) |
34 | 33 | imp 410 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) → (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
35 | | fveq2 6686 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → (rec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑥)) |
36 | 35 | sseq1d 3918 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑥 → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥) ↔ (rec(𝐹, 𝐴)‘𝑥) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
37 | 30, 36 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ On → (𝑦 = 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
38 | 37 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) → (𝑦 = 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
39 | 34, 38 | jaod 858 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) → ((𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥) → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
40 | 8, 39 | syl5bi 245 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) → (𝑦 ∈ suc 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
41 | 40 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → ((𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) → (𝑦 ∈ suc 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)))) |
42 | 41 | ralimdv2 3091 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → ∀𝑦 ∈ suc 𝑥(rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
43 | | df-sbc 3686 |
. . . . . . . . . . . . 13
⊢
([suc 𝑥 /
𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ suc 𝑥 ∈ {𝑥 ∣ ∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)}) |
44 | | vex 3404 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
45 | 44 | sucex 7557 |
. . . . . . . . . . . . . 14
⊢ suc 𝑥 ∈ V |
46 | | fveq2 6686 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = suc 𝑥 → (rec(𝐹, 𝐴)‘𝑧) = (rec(𝐹, 𝐴)‘suc 𝑥)) |
47 | 46 | sseq2d 3919 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = suc 𝑥 → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧) ↔ (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
48 | 47 | raleqbi1dv 3309 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = suc 𝑥 → (∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧) ↔ ∀𝑦 ∈ suc 𝑥(rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥))) |
49 | | fveq2 6686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → (rec(𝐹, 𝐴)‘𝑥) = (rec(𝐹, 𝐴)‘𝑧)) |
50 | 49 | sseq2d 3919 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧))) |
51 | 50 | raleqbi1dv 3309 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ ∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧))) |
52 | 51 | cbvabv 2807 |
. . . . . . . . . . . . . 14
⊢ {𝑥 ∣ ∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)} = {𝑧 ∣ ∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)} |
53 | 45, 48, 52 | elab2 3582 |
. . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ {𝑥 ∣ ∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)} ↔ ∀𝑦 ∈ suc 𝑥(rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)) |
54 | 43, 53 | bitri 278 |
. . . . . . . . . . . 12
⊢
([suc 𝑥 /
𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ ∀𝑦 ∈ suc 𝑥(rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘suc 𝑥)) |
55 | 42, 54 | syl6ibr 255 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → (∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → [suc 𝑥 / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) |
56 | | ssiun2 4943 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑧 → (rec(𝐹, 𝐴)‘𝑦) ⊆ ∪
𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦)) |
57 | 56 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝑧 ∧ 𝑦 ∈ 𝑧) → (rec(𝐹, 𝐴)‘𝑦) ⊆ ∪
𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦)) |
58 | | vex 3404 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
59 | | rdglim2a 8110 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ V ∧ Lim 𝑧) → (rec(𝐹, 𝐴)‘𝑧) = ∪ 𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦)) |
60 | 58, 59 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝑧 → (rec(𝐹, 𝐴)‘𝑧) = ∪ 𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦)) |
61 | 60 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝑧 ∧ 𝑦 ∈ 𝑧) → (rec(𝐹, 𝐴)‘𝑧) = ∪ 𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦)) |
62 | 57, 61 | sseqtrrd 3928 |
. . . . . . . . . . . . . 14
⊢ ((Lim
𝑧 ∧ 𝑦 ∈ 𝑧) → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)) |
63 | 62 | ralrimiva 3097 |
. . . . . . . . . . . . 13
⊢ (Lim
𝑧 → ∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)) |
64 | | df-sbc 3686 |
. . . . . . . . . . . . . . 15
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ 𝑧 ∈ {𝑥 ∣ ∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)}) |
65 | 52 | eleq2i 2825 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {𝑥 ∣ ∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)} ↔ 𝑧 ∈ {𝑧 ∣ ∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)}) |
66 | 64, 65 | bitri 278 |
. . . . . . . . . . . . . 14
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ 𝑧 ∈ {𝑧 ∣ ∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)}) |
67 | | abid 2721 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ {𝑧 ∣ ∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)} ↔ ∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)) |
68 | 66, 67 | bitri 278 |
. . . . . . . . . . . . 13
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ ∀𝑦 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑧)) |
69 | 63, 68 | sylibr 237 |
. . . . . . . . . . . 12
⊢ (Lim
𝑧 → [𝑧 / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) |
70 | 69 | a1d 25 |
. . . . . . . . . . 11
⊢ (Lim
𝑧 → (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → [𝑧 / 𝑥]∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) |
71 | 6, 55, 70 | tfindes 7608 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → ∀𝑦 ∈ 𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) |
72 | | rsp 3119 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝑥 (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) → (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) |
73 | 71, 72 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) |
74 | | eleq1 2821 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥 ∈ On ↔ 𝑋 ∈ On)) |
75 | 74 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑌 ∧ 𝑥 = 𝑋) → (𝑥 ∈ On ↔ 𝑋 ∈ On)) |
76 | | eleq12 2823 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑌 ∧ 𝑥 = 𝑋) → (𝑦 ∈ 𝑥 ↔ 𝑌 ∈ 𝑋)) |
77 | | fveq2 6686 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → (rec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑌)) |
78 | 77 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝑌 ∧ 𝑥 = 𝑋) → (rec(𝐹, 𝐴)‘𝑦) = (rec(𝐹, 𝐴)‘𝑌)) |
79 | | fveq2 6686 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (rec(𝐹, 𝐴)‘𝑥) = (rec(𝐹, 𝐴)‘𝑋)) |
80 | 79 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑦 = 𝑌 ∧ 𝑥 = 𝑋) → (rec(𝐹, 𝐴)‘𝑥) = (rec(𝐹, 𝐴)‘𝑋)) |
81 | 78, 80 | sseq12d 3920 |
. . . . . . . . . . 11
⊢ ((𝑦 = 𝑌 ∧ 𝑥 = 𝑋) → ((rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥) ↔ (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))) |
82 | 76, 81 | imbi12d 348 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑌 ∧ 𝑥 = 𝑋) → ((𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥)) ↔ (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))) |
83 | 75, 82 | imbi12d 348 |
. . . . . . . . 9
⊢ ((𝑦 = 𝑌 ∧ 𝑥 = 𝑋) → ((𝑥 ∈ On → (𝑦 ∈ 𝑥 → (rec(𝐹, 𝐴)‘𝑦) ⊆ (rec(𝐹, 𝐴)‘𝑥))) ↔ (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))))) |
84 | 73, 83 | mpbii 236 |
. . . . . . . 8
⊢ ((𝑦 = 𝑌 ∧ 𝑥 = 𝑋) → (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))) |
85 | 84 | ex 416 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (𝑥 = 𝑋 → (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))))) |
86 | 85 | vtocleg 3489 |
. . . . . 6
⊢ (𝑌 ∈ 𝑋 → (𝑥 = 𝑋 → (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))))) |
87 | 86 | com12 32 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑌 ∈ 𝑋 → (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))))) |
88 | 87 | vtocleg 3489 |
. . . 4
⊢ (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))))) |
89 | 88 | pm2.43b 55 |
. . 3
⊢ (𝑌 ∈ 𝑋 → (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)))) |
90 | 89 | pm2.43b 55 |
. 2
⊢ (𝑋 ∈ On → (𝑌 ∈ 𝑋 → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋))) |
91 | 90 | imp 410 |
1
⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ 𝑋) → (rec(𝐹, 𝐴)‘𝑌) ⊆ (rec(𝐹, 𝐴)‘𝑋)) |