Step |
Hyp |
Ref |
Expression |
1 |
|
fmla0 |
⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) } |
2 |
|
rabab |
⊢ { 𝑥 ∈ V ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) } = { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) } |
3 |
1 2
|
eqtri |
⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) } |
4 |
3
|
ineq1i |
⊢ ( ( Fmla ‘ ∅ ) ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = ( { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) } ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) |
5 |
|
inab |
⊢ ( { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) } ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = { 𝑥 ∣ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ∧ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) } |
6 |
|
goel |
⊢ ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑗 ∈𝑔 𝑘 ) = 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 ) |
7 |
6
|
eqeq2d |
⊢ ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ↔ 𝑥 = 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 ) ) |
8 |
|
1n0 |
⊢ 1o ≠ ∅ |
9 |
8
|
nesymi |
⊢ ¬ ∅ = 1o |
10 |
9
|
intnanr |
⊢ ¬ ( ∅ = 1o ∧ 〈 𝑗 , 𝑘 〉 = 〈 𝑢 , 𝑣 〉 ) |
11 |
|
gonafv |
⊢ ( ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) → ( 𝑢 ⊼𝑔 𝑣 ) = 〈 1o , 〈 𝑢 , 𝑣 〉 〉 ) |
12 |
11
|
el2v |
⊢ ( 𝑢 ⊼𝑔 𝑣 ) = 〈 1o , 〈 𝑢 , 𝑣 〉 〉 |
13 |
12
|
eqeq2i |
⊢ ( 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = 〈 1o , 〈 𝑢 , 𝑣 〉 〉 ) |
14 |
|
0ex |
⊢ ∅ ∈ V |
15 |
|
opex |
⊢ 〈 𝑗 , 𝑘 〉 ∈ V |
16 |
14 15
|
opth |
⊢ ( 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = 〈 1o , 〈 𝑢 , 𝑣 〉 〉 ↔ ( ∅ = 1o ∧ 〈 𝑗 , 𝑘 〉 = 〈 𝑢 , 𝑣 〉 ) ) |
17 |
13 16
|
bitri |
⊢ ( 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ( ∅ = 1o ∧ 〈 𝑗 , 𝑘 〉 = 〈 𝑢 , 𝑣 〉 ) ) |
18 |
10 17
|
mtbir |
⊢ ¬ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = ( 𝑢 ⊼𝑔 𝑣 ) |
19 |
|
eqeq1 |
⊢ ( 𝑥 = 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 → ( 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = ( 𝑢 ⊼𝑔 𝑣 ) ) ) |
20 |
18 19
|
mtbiri |
⊢ ( 𝑥 = 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 → ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) |
21 |
7 20
|
syl6bi |
⊢ ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) → ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) ) |
22 |
21
|
imp |
⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) → ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) |
23 |
22
|
adantr |
⊢ ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) |
24 |
23
|
ralrimivw |
⊢ ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) |
25 |
|
2on0 |
⊢ 2o ≠ ∅ |
26 |
25
|
nesymi |
⊢ ¬ ∅ = 2o |
27 |
26
|
orci |
⊢ ( ¬ ∅ = 2o ∨ ¬ 〈 𝑗 , 𝑘 〉 = 〈 𝑖 , 𝑢 〉 ) |
28 |
14 15
|
opth |
⊢ ( 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 ↔ ( ∅ = 2o ∧ 〈 𝑗 , 𝑘 〉 = 〈 𝑖 , 𝑢 〉 ) ) |
29 |
28
|
notbii |
⊢ ( ¬ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 ↔ ¬ ( ∅ = 2o ∧ 〈 𝑗 , 𝑘 〉 = 〈 𝑖 , 𝑢 〉 ) ) |
30 |
|
ianor |
⊢ ( ¬ ( ∅ = 2o ∧ 〈 𝑗 , 𝑘 〉 = 〈 𝑖 , 𝑢 〉 ) ↔ ( ¬ ∅ = 2o ∨ ¬ 〈 𝑗 , 𝑘 〉 = 〈 𝑖 , 𝑢 〉 ) ) |
31 |
29 30
|
bitri |
⊢ ( ¬ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 ↔ ( ¬ ∅ = 2o ∨ ¬ 〈 𝑗 , 𝑘 〉 = 〈 𝑖 , 𝑢 〉 ) ) |
32 |
27 31
|
mpbir |
⊢ ¬ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 |
33 |
|
eqeq1 |
⊢ ( 𝑥 = 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 → ( 𝑥 = ∀𝑔 𝑖 𝑢 ↔ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = ∀𝑔 𝑖 𝑢 ) ) |
34 |
|
df-goal |
⊢ ∀𝑔 𝑖 𝑢 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 |
35 |
34
|
eqeq2i |
⊢ ( 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = ∀𝑔 𝑖 𝑢 ↔ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 ) |
36 |
33 35
|
bitrdi |
⊢ ( 𝑥 = 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 → ( 𝑥 = ∀𝑔 𝑖 𝑢 ↔ 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 = 〈 2o , 〈 𝑖 , 𝑢 〉 〉 ) ) |
37 |
32 36
|
mtbiri |
⊢ ( 𝑥 = 〈 ∅ , 〈 𝑗 , 𝑘 〉 〉 → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) |
38 |
7 37
|
syl6bi |
⊢ ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
39 |
38
|
imp |
⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) |
40 |
39
|
adantr |
⊢ ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) |
41 |
40
|
adantr |
⊢ ( ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) ∧ 𝑖 ∈ ω ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) |
42 |
41
|
ralrimiva |
⊢ ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) |
43 |
24 42
|
jca |
⊢ ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
44 |
43
|
ralrimiva |
⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) → ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
45 |
|
ralnex |
⊢ ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ↔ ¬ ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) |
46 |
|
ralnex |
⊢ ( ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ¬ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) |
47 |
45 46
|
anbi12i |
⊢ ( ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ¬ ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ¬ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
48 |
|
ioran |
⊢ ( ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ¬ ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ¬ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
49 |
47 48
|
bitr4i |
⊢ ( ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
50 |
49
|
ralbii |
⊢ ( ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
51 |
|
ralnex |
⊢ ( ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
52 |
50 51
|
bitri |
⊢ ( ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
53 |
44 52
|
sylib |
⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
54 |
53
|
ex |
⊢ ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) |
55 |
54
|
rexlimdva |
⊢ ( 𝑗 ∈ ω → ( ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) |
56 |
55
|
rexlimiv |
⊢ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
57 |
56
|
imori |
⊢ ( ¬ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ∨ ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
58 |
|
ianor |
⊢ ( ¬ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ∧ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ↔ ( ¬ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ∨ ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ) |
59 |
57 58
|
mpbir |
⊢ ¬ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ∧ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) |
60 |
59
|
abf |
⊢ { 𝑥 ∣ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) ∧ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) } = ∅ |
61 |
5 60
|
eqtri |
⊢ ( { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) } ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = ∅ |
62 |
4 61
|
eqtri |
⊢ ( ( Fmla ‘ ∅ ) ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = ∅ |