Step |
Hyp |
Ref |
Expression |
1 |
|
fmlasuc0 |
⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) } ) ) |
2 |
|
eqid |
⊢ ( ∅ Sat ∅ ) = ( ∅ Sat ∅ ) |
3 |
2
|
satf0op |
⊢ ( 𝑁 ∈ ω → ( 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ↔ ∃ 𝑧 ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ) |
4 |
|
fveq2 |
⊢ ( 𝑧 = 𝑤 → ( 1st ‘ 𝑧 ) = ( 1st ‘ 𝑤 ) ) |
5 |
4
|
oveq2d |
⊢ ( 𝑧 = 𝑤 → ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) |
6 |
5
|
eqeq2d |
⊢ ( 𝑧 = 𝑤 → ( 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ↔ 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) ) |
7 |
6
|
cbvrexvw |
⊢ ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ↔ ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) |
8 |
7
|
orbi1i |
⊢ ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) |
9 |
|
fmlafvel |
⊢ ( 𝑁 ∈ ω → ( 𝑧 ∈ ( Fmla ‘ 𝑁 ) ↔ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
10 |
9
|
biimprd |
⊢ ( 𝑁 ∈ ω → ( 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) ) |
11 |
10
|
adantld |
⊢ ( 𝑁 ∈ ω → ( ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) ) |
12 |
11
|
imp |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) |
13 |
|
vex |
⊢ 𝑧 ∈ V |
14 |
|
0ex |
⊢ ∅ ∈ V |
15 |
13 14
|
op1std |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( 1st ‘ 𝑦 ) = 𝑧 ) |
16 |
15
|
eleq1d |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( ( 1st ‘ 𝑦 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) ) |
17 |
16
|
ad2antrl |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( 1st ‘ 𝑦 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑧 ∈ ( Fmla ‘ 𝑁 ) ) ) |
18 |
12 17
|
mpbird |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( 1st ‘ 𝑦 ) ∈ ( Fmla ‘ 𝑁 ) ) |
19 |
18
|
3adant3 |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) → ( 1st ‘ 𝑦 ) ∈ ( Fmla ‘ 𝑁 ) ) |
20 |
|
oveq1 |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → ( 𝑢 ⊼𝑔 𝑣 ) = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ) |
21 |
20
|
eqeq2d |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → ( 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ) ) |
22 |
21
|
rexbidv |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ) ) |
23 |
|
eqidd |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → 𝑖 = 𝑖 ) |
24 |
|
id |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → 𝑢 = ( 1st ‘ 𝑦 ) ) |
25 |
23 24
|
goaleq12d |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → ∀𝑔 𝑖 𝑢 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) |
26 |
25
|
eqeq2d |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → ( 𝑥 = ∀𝑔 𝑖 𝑢 ↔ 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) |
27 |
26
|
rexbidv |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) |
28 |
22 27
|
orbi12d |
⊢ ( 𝑢 = ( 1st ‘ 𝑦 ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) ) |
29 |
28
|
adantl |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) ∧ 𝑢 = ( 1st ‘ 𝑦 ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) ) |
30 |
2
|
satf0op |
⊢ ( 𝑁 ∈ ω → ( 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ↔ ∃ 𝑦 ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ) |
31 |
|
fmlafvel |
⊢ ( 𝑁 ∈ ω → ( 𝑦 ∈ ( Fmla ‘ 𝑁 ) ↔ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
32 |
31
|
biimprd |
⊢ ( 𝑁 ∈ ω → ( 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) ) |
33 |
32
|
adantld |
⊢ ( 𝑁 ∈ ω → ( ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) ) |
34 |
33
|
imp |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) |
35 |
|
vex |
⊢ 𝑦 ∈ V |
36 |
35 14
|
op1std |
⊢ ( 𝑤 = 〈 𝑦 , ∅ 〉 → ( 1st ‘ 𝑤 ) = 𝑦 ) |
37 |
36
|
eleq1d |
⊢ ( 𝑤 = 〈 𝑦 , ∅ 〉 → ( ( 1st ‘ 𝑤 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) ) |
38 |
37
|
ad2antrl |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( 1st ‘ 𝑤 ) ∈ ( Fmla ‘ 𝑁 ) ↔ 𝑦 ∈ ( Fmla ‘ 𝑁 ) ) ) |
39 |
34 38
|
mpbird |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( 1st ‘ 𝑤 ) ∈ ( Fmla ‘ 𝑁 ) ) |
40 |
39
|
adantr |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) → ( 1st ‘ 𝑤 ) ∈ ( Fmla ‘ 𝑁 ) ) |
41 |
|
oveq2 |
⊢ ( 𝑣 = ( 1st ‘ 𝑤 ) → ( 𝑧 ⊼𝑔 𝑣 ) = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) |
42 |
41
|
eqeq2d |
⊢ ( 𝑣 = ( 1st ‘ 𝑤 ) → ( 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) ) |
43 |
42
|
adantl |
⊢ ( ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) ∧ 𝑣 = ( 1st ‘ 𝑤 ) ) → ( 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) ) |
44 |
|
simpr |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) → 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) |
45 |
40 43 44
|
rspcedvd |
⊢ ( ( ( 𝑁 ∈ ω ∧ ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) ∧ 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) |
46 |
45
|
exp31 |
⊢ ( 𝑁 ∈ ω → ( ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) ) |
47 |
46
|
exlimdv |
⊢ ( 𝑁 ∈ ω → ( ∃ 𝑦 ( 𝑤 = 〈 𝑦 , ∅ 〉 ∧ 〈 𝑦 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) ) |
48 |
30 47
|
sylbid |
⊢ ( 𝑁 ∈ ω → ( 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) ) |
49 |
48
|
rexlimdv |
⊢ ( 𝑁 ∈ ω → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) |
50 |
49
|
adantr |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) |
51 |
15
|
oveq1d |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) |
52 |
51
|
eqeq2d |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ↔ 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) ) |
53 |
52
|
rexbidv |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ↔ ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) ) ) |
54 |
15
|
oveq1d |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) = ( 𝑧 ⊼𝑔 𝑣 ) ) |
55 |
54
|
eqeq2d |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ↔ 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) |
56 |
55
|
rexbidv |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ↔ ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) |
57 |
53 56
|
imbi12d |
⊢ ( 𝑦 = 〈 𝑧 , ∅ 〉 → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) ) |
58 |
57
|
ad2antrl |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ) ↔ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑧 ⊼𝑔 𝑣 ) ) ) ) |
59 |
50 58
|
mpbird |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) → ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ) ) |
60 |
59
|
orim1d |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) ) |
61 |
60
|
3impia |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) |
62 |
19 29 61
|
rspcedvd |
⊢ ( ( 𝑁 ∈ ω ∧ ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ∧ ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
63 |
62
|
3exp |
⊢ ( 𝑁 ∈ ω → ( ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) ) |
64 |
63
|
exlimdv |
⊢ ( 𝑁 ∈ ω → ( ∃ 𝑧 ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑤 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑤 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) ) |
65 |
8 64
|
syl7bi |
⊢ ( 𝑁 ∈ ω → ( ∃ 𝑧 ( 𝑦 = 〈 𝑧 , ∅ 〉 ∧ 〈 𝑧 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) ) |
66 |
3 65
|
sylbid |
⊢ ( 𝑁 ∈ ω → ( 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) ) |
67 |
66
|
rexlimdv |
⊢ ( 𝑁 ∈ ω → ( ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) → ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) |
68 |
|
fmlafvel |
⊢ ( 𝑁 ∈ ω → ( 𝑢 ∈ ( Fmla ‘ 𝑁 ) ↔ 〈 𝑢 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
69 |
68
|
biimpa |
⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → 〈 𝑢 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
70 |
69
|
adantr |
⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) → 〈 𝑢 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
71 |
|
vex |
⊢ 𝑢 ∈ V |
72 |
71 14
|
op1std |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → ( 1st ‘ 𝑦 ) = 𝑢 ) |
73 |
72
|
oveq1d |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ) |
74 |
73
|
eqeq2d |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → ( 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ) ) |
75 |
74
|
rexbidv |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ↔ ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ) ) |
76 |
|
eqidd |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → 𝑖 = 𝑖 ) |
77 |
76 72
|
goaleq12d |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) = ∀𝑔 𝑖 𝑢 ) |
78 |
77
|
eqeq2d |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ↔ 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
79 |
78
|
rexbidv |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
80 |
75 79
|
orbi12d |
⊢ ( 𝑦 = 〈 𝑢 , ∅ 〉 → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ↔ ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) |
81 |
80
|
adantl |
⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ∧ 𝑦 = 〈 𝑢 , ∅ 〉 ) → ( ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ↔ ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) |
82 |
|
fmlafvel |
⊢ ( 𝑁 ∈ ω → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) ↔ 〈 𝑣 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
83 |
82
|
biimpd |
⊢ ( 𝑁 ∈ ω → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) → 〈 𝑣 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
84 |
83
|
adantr |
⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( 𝑣 ∈ ( Fmla ‘ 𝑁 ) → 〈 𝑣 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) ) |
85 |
84
|
imp |
⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) → 〈 𝑣 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
86 |
85
|
adantr |
⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) → 〈 𝑣 , ∅ 〉 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) |
87 |
|
vex |
⊢ 𝑣 ∈ V |
88 |
87 14
|
op1std |
⊢ ( 𝑧 = 〈 𝑣 , ∅ 〉 → ( 1st ‘ 𝑧 ) = 𝑣 ) |
89 |
88
|
oveq2d |
⊢ ( 𝑧 = 〈 𝑣 , ∅ 〉 → ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) = ( 𝑢 ⊼𝑔 𝑣 ) ) |
90 |
89
|
eqeq2d |
⊢ ( 𝑧 = 〈 𝑣 , ∅ 〉 → ( 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) ) |
91 |
90
|
adantl |
⊢ ( ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) ∧ 𝑧 = 〈 𝑣 , ∅ 〉 ) → ( 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ↔ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) ) |
92 |
|
simpr |
⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) → 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) |
93 |
86 91 92
|
rspcedvd |
⊢ ( ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( Fmla ‘ 𝑁 ) ) ∧ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) → ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ) |
94 |
93
|
rexlimdva2 |
⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) → ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ) ) |
95 |
94
|
orim1d |
⊢ ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) → ( ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) |
96 |
95
|
imp |
⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) → ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
97 |
70 81 96
|
rspcedvd |
⊢ ( ( ( 𝑁 ∈ ω ∧ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ) ∧ ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) → ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) |
98 |
97
|
rexlimdva2 |
⊢ ( 𝑁 ∈ ω → ( ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) → ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ) ) |
99 |
67 98
|
impbid |
⊢ ( 𝑁 ∈ ω → ( ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) ↔ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) |
100 |
99
|
abbidv |
⊢ ( 𝑁 ∈ ω → { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) |
101 |
100
|
uneq2d |
⊢ ( 𝑁 ∈ ω → ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ( ∃ 𝑧 ∈ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑦 ) ⊼𝑔 ( 1st ‘ 𝑧 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑦 ) ) } ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) ) |
102 |
1 101
|
eqtrd |
⊢ ( 𝑁 ∈ ω → ( Fmla ‘ suc 𝑁 ) = ( ( Fmla ‘ 𝑁 ) ∪ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( Fmla ‘ 𝑁 ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) ) |