Step |
Hyp |
Ref |
Expression |
1 |
|
axdclem.1 |
⊢ 𝐹 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) ) , 𝑠 ) ↾ ω ) |
2 |
|
neeq1 |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( 𝑦 ≠ ∅ ↔ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ≠ ∅ ) ) |
3 |
|
abn0 |
⊢ ( { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ≠ ∅ ↔ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) |
4 |
2 3
|
bitrdi |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( 𝑦 ≠ ∅ ↔ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) ) |
5 |
|
eleq2 |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑔 ‘ 𝑦 ) ∈ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) |
6 |
|
breq2 |
⊢ ( 𝑤 = 𝑧 → ( ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) ) |
7 |
6
|
cbvabv |
⊢ { 𝑤 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 } = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } |
8 |
7
|
eleq2i |
⊢ ( ( 𝑔 ‘ 𝑦 ) ∈ { 𝑤 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 } ↔ ( 𝑔 ‘ 𝑦 ) ∈ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) |
9 |
5 8
|
bitr4di |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝑔 ‘ 𝑦 ) ∈ { 𝑤 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 } ) ) |
10 |
|
fvex |
⊢ ( 𝑔 ‘ 𝑦 ) ∈ V |
11 |
|
breq2 |
⊢ ( 𝑤 = ( 𝑔 ‘ 𝑦 ) → ( ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ 𝑦 ) ) ) |
12 |
10 11
|
elab |
⊢ ( ( 𝑔 ‘ 𝑦 ) ∈ { 𝑤 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑤 } ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ 𝑦 ) ) |
13 |
9 12
|
bitrdi |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ 𝑦 ) ) ) |
14 |
|
fveq2 |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) |
15 |
14
|
breq2d |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) |
16 |
13 15
|
bitrd |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) |
17 |
4 16
|
imbi12d |
⊢ ( 𝑦 = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } → ( ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ↔ ( ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) ) |
18 |
17
|
rspcv |
⊢ ( { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ∈ 𝒫 dom 𝑥 → ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) ) |
19 |
|
fvex |
⊢ ( 𝐹 ‘ 𝐾 ) ∈ V |
20 |
|
vex |
⊢ 𝑧 ∈ V |
21 |
19 20
|
brelrn |
⊢ ( ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 → 𝑧 ∈ ran 𝑥 ) |
22 |
21
|
abssi |
⊢ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ ran 𝑥 |
23 |
|
sstr |
⊢ ( ( { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ ran 𝑥 ∧ ran 𝑥 ⊆ dom 𝑥 ) → { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ dom 𝑥 ) |
24 |
22 23
|
mpan |
⊢ ( ran 𝑥 ⊆ dom 𝑥 → { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ dom 𝑥 ) |
25 |
|
vex |
⊢ 𝑥 ∈ V |
26 |
25
|
dmex |
⊢ dom 𝑥 ∈ V |
27 |
26
|
elpw2 |
⊢ ( { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ∈ 𝒫 dom 𝑥 ↔ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ⊆ dom 𝑥 ) |
28 |
24 27
|
sylibr |
⊢ ( ran 𝑥 ⊆ dom 𝑥 → { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ∈ 𝒫 dom 𝑥 ) |
29 |
18 28
|
syl11 |
⊢ ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) → ( ran 𝑥 ⊆ dom 𝑥 → ( ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) ) |
30 |
29
|
3imp |
⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) |
31 |
|
fvex |
⊢ ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ∈ V |
32 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑠 |
33 |
|
nfcv |
⊢ Ⅎ 𝑦 𝐾 |
34 |
|
nfcv |
⊢ Ⅎ 𝑦 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) |
35 |
|
breq1 |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝐾 ) → ( 𝑦 𝑥 𝑧 ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) ) |
36 |
35
|
abbidv |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝐾 ) → { 𝑧 ∣ 𝑦 𝑥 𝑧 } = { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) |
37 |
36
|
fveq2d |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝐾 ) → ( 𝑔 ‘ { 𝑧 ∣ 𝑦 𝑥 𝑧 } ) = ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) |
38 |
32 33 34 1 37
|
frsucmpt |
⊢ ( ( 𝐾 ∈ ω ∧ ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ∈ V ) → ( 𝐹 ‘ suc 𝐾 ) = ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) |
39 |
31 38
|
mpan2 |
⊢ ( 𝐾 ∈ ω → ( 𝐹 ‘ suc 𝐾 ) = ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) |
40 |
39
|
breq2d |
⊢ ( 𝐾 ∈ ω → ( ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝐹 ‘ suc 𝐾 ) ↔ ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝑔 ‘ { 𝑧 ∣ ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 } ) ) ) |
41 |
30 40
|
syl5ibrcom |
⊢ ( ( ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( 𝑦 ≠ ∅ → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ∧ ran 𝑥 ⊆ dom 𝑥 ∧ ∃ 𝑧 ( 𝐹 ‘ 𝐾 ) 𝑥 𝑧 ) → ( 𝐾 ∈ ω → ( 𝐹 ‘ 𝐾 ) 𝑥 ( 𝐹 ‘ suc 𝐾 ) ) ) |