Step | Hyp | Ref
| Expression |
1 | | fveq2 5178 |
. . . . 5
⊢ (𝑧 = 𝑥 → (rec(𝐹, 𝐴)‘𝑧) = (rec(𝐹, 𝐴)‘𝑥)) |
2 | 1 | eleq1d 2106 |
. . . 4
⊢ (𝑧 = 𝑥 → ((rec(𝐹, 𝐴)‘𝑧) ∈ On ↔ (rec(𝐹, 𝐴)‘𝑥) ∈ On)) |
3 | 2 | imbi2d 219 |
. . 3
⊢ (𝑧 = 𝑥 → ((𝜑 → (rec(𝐹, 𝐴)‘𝑧) ∈ On) ↔ (𝜑 → (rec(𝐹, 𝐴)‘𝑥) ∈ On))) |
4 | | fveq2 5178 |
. . . . 5
⊢ (𝑧 = 𝐵 → (rec(𝐹, 𝐴)‘𝑧) = (rec(𝐹, 𝐴)‘𝐵)) |
5 | 4 | eleq1d 2106 |
. . . 4
⊢ (𝑧 = 𝐵 → ((rec(𝐹, 𝐴)‘𝑧) ∈ On ↔ (rec(𝐹, 𝐴)‘𝐵) ∈ On)) |
6 | 5 | imbi2d 219 |
. . 3
⊢ (𝑧 = 𝐵 → ((𝜑 → (rec(𝐹, 𝐴)‘𝑧) ∈ On) ↔ (𝜑 → (rec(𝐹, 𝐴)‘𝐵) ∈ On))) |
7 | | r19.21v 2396 |
. . . 4
⊢
(∀𝑥 ∈
𝑧 (𝜑 → (rec(𝐹, 𝐴)‘𝑥) ∈ On) ↔ (𝜑 → ∀𝑥 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑥) ∈ On)) |
8 | | rdgon.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ On) |
9 | | fvres 5198 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑧 → ((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥) = (rec(𝐹, 𝐴)‘𝑥)) |
10 | 9 | eleq1d 2106 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑧 → (((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥) ∈ On ↔ (rec(𝐹, 𝐴)‘𝑥) ∈ On)) |
11 | 10 | adantl 262 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑧) → (((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥) ∈ On ↔ (rec(𝐹, 𝐴)‘𝑥) ∈ On)) |
12 | | rdgon.3 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ On (𝐹‘𝑥) ∈ On) |
13 | | fveq2 5178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤)) |
14 | 13 | eleq1d 2106 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → ((𝐹‘𝑥) ∈ On ↔ (𝐹‘𝑤) ∈ On)) |
15 | 14 | cbvralv 2533 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈ On
(𝐹‘𝑥) ∈ On ↔ ∀𝑤 ∈ On (𝐹‘𝑤) ∈ On) |
16 | 12, 15 | sylib 127 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑤 ∈ On (𝐹‘𝑤) ∈ On) |
17 | | fveq2 5178 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = ((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥) → (𝐹‘𝑤) = (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥))) |
18 | 17 | eleq1d 2106 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = ((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥) → ((𝐹‘𝑤) ∈ On ↔ (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On)) |
19 | 18 | rspcv 2652 |
. . . . . . . . . . . . . 14
⊢
(((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥) ∈ On → (∀𝑤 ∈ On (𝐹‘𝑤) ∈ On → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On)) |
20 | 16, 19 | syl5com 26 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥) ∈ On → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On)) |
21 | 20 | adantr 261 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑧) → (((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥) ∈ On → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On)) |
22 | 11, 21 | sylbird 159 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑧) → ((rec(𝐹, 𝐴)‘𝑥) ∈ On → (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On)) |
23 | 22 | ralimdva 2387 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑥 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑥) ∈ On → ∀𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On)) |
24 | | vex 2560 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
25 | | iunon 5899 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ V ∧ ∀𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On) → ∪ 𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On) |
26 | 24, 25 | mpan 400 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On → ∪ 𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On) |
27 | 23, 26 | syl6 29 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑥 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑥) ∈ On → ∪ 𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On)) |
28 | | onun2 4216 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ ∪ 𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)) ∈ On) → (𝐴 ∪ ∪
𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥))) ∈ On) |
29 | 8, 27, 28 | syl6an 1323 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑥 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑥) ∈ On → (𝐴 ∪ ∪
𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥))) ∈ On)) |
30 | 29 | adantr 261 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑥 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑥) ∈ On → (𝐴 ∪ ∪
𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥))) ∈ On)) |
31 | | rdgon.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 Fn V) |
32 | 31, 8 | jca 290 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 Fn V ∧ 𝐴 ∈ On)) |
33 | | rdgivallem 5968 |
. . . . . . . . . 10
⊢ ((𝐹 Fn V ∧ 𝐴 ∈ On ∧ 𝑧 ∈ On) → (rec(𝐹, 𝐴)‘𝑧) = (𝐴 ∪ ∪
𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)))) |
34 | 33 | 3expa 1104 |
. . . . . . . . 9
⊢ (((𝐹 Fn V ∧ 𝐴 ∈ On) ∧ 𝑧 ∈ On) → (rec(𝐹, 𝐴)‘𝑧) = (𝐴 ∪ ∪
𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)))) |
35 | 32, 34 | sylan 267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (rec(𝐹, 𝐴)‘𝑧) = (𝐴 ∪ ∪
𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥)))) |
36 | 35 | eleq1d 2106 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ On) → ((rec(𝐹, 𝐴)‘𝑧) ∈ On ↔ (𝐴 ∪ ∪
𝑥 ∈ 𝑧 (𝐹‘((rec(𝐹, 𝐴) ↾ 𝑧)‘𝑥))) ∈ On)) |
37 | 30, 36 | sylibrd 158 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ On) → (∀𝑥 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑥) ∈ On → (rec(𝐹, 𝐴)‘𝑧) ∈ On)) |
38 | 37 | expcom 109 |
. . . . 5
⊢ (𝑧 ∈ On → (𝜑 → (∀𝑥 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑥) ∈ On → (rec(𝐹, 𝐴)‘𝑧) ∈ On))) |
39 | 38 | a2d 23 |
. . . 4
⊢ (𝑧 ∈ On → ((𝜑 → ∀𝑥 ∈ 𝑧 (rec(𝐹, 𝐴)‘𝑥) ∈ On) → (𝜑 → (rec(𝐹, 𝐴)‘𝑧) ∈ On))) |
40 | 7, 39 | syl5bi 141 |
. . 3
⊢ (𝑧 ∈ On → (∀𝑥 ∈ 𝑧 (𝜑 → (rec(𝐹, 𝐴)‘𝑥) ∈ On) → (𝜑 → (rec(𝐹, 𝐴)‘𝑧) ∈ On))) |
41 | 3, 6, 40 | tfis3 4309 |
. 2
⊢ (𝐵 ∈ On → (𝜑 → (rec(𝐹, 𝐴)‘𝐵) ∈ On)) |
42 | 41 | impcom 116 |
1
⊢ ((𝜑 ∧ 𝐵 ∈ On) → (rec(𝐹, 𝐴)‘𝐵) ∈ On) |