Step |
Hyp |
Ref |
Expression |
1 |
|
satfv1fvfmla1.x |
⊢ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) |
2 |
|
simpll |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐼 ∈ ω ) |
3 |
|
simplr |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐽 ∈ ω ) |
4 |
|
simprl |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐾 ∈ ω ) |
5 |
|
simprr |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐿 ∈ ω ) |
6 |
|
oveq2 |
⊢ ( 𝑛 = 𝐿 → ( 𝐾 ∈𝑔 𝑛 ) = ( 𝐾 ∈𝑔 𝐿 ) ) |
7 |
6
|
oveq2d |
⊢ ( 𝑛 = 𝐿 → ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ) |
8 |
7
|
eqeq2d |
⊢ ( 𝑛 = 𝐿 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ) ) |
9 |
8
|
adantl |
⊢ ( ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑛 = 𝐿 ) → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ) ) |
10 |
1
|
a1i |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ) |
11 |
5 9 10
|
rspcedvd |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ) |
12 |
11
|
orcd |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) ) |
13 |
|
oveq1 |
⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∈𝑔 𝑗 ) = ( 𝐼 ∈𝑔 𝑗 ) ) |
14 |
13
|
oveq1d |
⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) |
15 |
14
|
eqeq2d |
⊢ ( 𝑖 = 𝐼 → ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) ) |
16 |
15
|
rexbidv |
⊢ ( 𝑖 = 𝐼 → ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) ) |
17 |
|
eqidd |
⊢ ( 𝑖 = 𝐼 → 𝑘 = 𝑘 ) |
18 |
17 13
|
goaleq12d |
⊢ ( 𝑖 = 𝐼 → ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ) |
19 |
18
|
eqeq2d |
⊢ ( 𝑖 = 𝐼 → ( 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ) ) |
20 |
16 19
|
orbi12d |
⊢ ( 𝑖 = 𝐼 → ( ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ) ) ) |
21 |
|
oveq2 |
⊢ ( 𝑗 = 𝐽 → ( 𝐼 ∈𝑔 𝑗 ) = ( 𝐼 ∈𝑔 𝐽 ) ) |
22 |
21
|
oveq1d |
⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) |
23 |
22
|
eqeq2d |
⊢ ( 𝑗 = 𝐽 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) ) |
24 |
23
|
rexbidv |
⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) ) |
25 |
|
eqidd |
⊢ ( 𝑗 = 𝐽 → 𝑘 = 𝑘 ) |
26 |
25 21
|
goaleq12d |
⊢ ( 𝑗 = 𝐽 → ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ) |
27 |
26
|
eqeq2d |
⊢ ( 𝑗 = 𝐽 → ( 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ) ) |
28 |
24 27
|
orbi12d |
⊢ ( 𝑗 = 𝐽 → ( ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ) ) ) |
29 |
|
oveq1 |
⊢ ( 𝑘 = 𝐾 → ( 𝑘 ∈𝑔 𝑛 ) = ( 𝐾 ∈𝑔 𝑛 ) ) |
30 |
29
|
oveq2d |
⊢ ( 𝑘 = 𝐾 → ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ) |
31 |
30
|
eqeq2d |
⊢ ( 𝑘 = 𝐾 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ) ) |
32 |
31
|
rexbidv |
⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ) ) |
33 |
|
id |
⊢ ( 𝑘 = 𝐾 → 𝑘 = 𝐾 ) |
34 |
|
eqidd |
⊢ ( 𝑘 = 𝐾 → ( 𝐼 ∈𝑔 𝐽 ) = ( 𝐼 ∈𝑔 𝐽 ) ) |
35 |
33 34
|
goaleq12d |
⊢ ( 𝑘 = 𝐾 → ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) |
36 |
35
|
eqeq2d |
⊢ ( 𝑘 = 𝐾 → ( 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ↔ 𝑋 = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) ) |
37 |
32 36
|
orbi12d |
⊢ ( 𝑘 = 𝐾 → ( ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝐼 ∈𝑔 𝐽 ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) ) ) |
38 |
20 28 37
|
rspc3ev |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐾 ∈ ω ) ∧ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝐾 ( 𝐼 ∈𝑔 𝐽 ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) |
39 |
2 3 4 12 38
|
syl31anc |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) |
40 |
1
|
ovexi |
⊢ 𝑋 ∈ V |
41 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) ) |
42 |
41
|
rexbidv |
⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ↔ ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ) ) |
43 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) |
44 |
42 43
|
orbi12d |
⊢ ( 𝑥 = 𝑋 → ( ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) ) |
45 |
44
|
rexbidv |
⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) ) |
46 |
45
|
2rexbidv |
⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) ) |
47 |
40 46
|
elab |
⊢ ( 𝑋 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑋 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) ) |
48 |
39 47
|
sylibr |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) |
49 |
48
|
olcd |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑋 ∈ ( { ∅ } × ( ω × ω ) ) ∨ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) ) |
50 |
|
elun |
⊢ ( 𝑋 ∈ ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) ↔ ( 𝑋 ∈ ( { ∅ } × ( ω × ω ) ) ∨ 𝑋 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) ) |
51 |
49 50
|
sylibr |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) ) |
52 |
|
fmla1 |
⊢ ( Fmla ‘ 1o ) = ( ( { ∅ } × ( ω × ω ) ) ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω ( ∃ 𝑛 ∈ ω 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑛 ) ) ∨ 𝑥 = ∀𝑔 𝑘 ( 𝑖 ∈𝑔 𝑗 ) ) } ) |
53 |
51 52
|
eleqtrrdi |
⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ ( Fmla ‘ 1o ) ) |