Step |
Hyp |
Ref |
Expression |
1 |
|
satfv0.s |
⊢ 𝑆 = ( 𝑀 Sat 𝐸 ) |
2 |
|
ancom |
⊢ ( ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∧ 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ) ↔ ( 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ) ) |
3 |
2
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∧ 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ) } |
4 |
|
ovex |
⊢ ( 𝑀 ↑m ω ) ∈ V |
5 |
4
|
pwex |
⊢ 𝒫 ( 𝑀 ↑m ω ) ∈ V |
6 |
5
|
a1i |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → 𝒫 ( 𝑀 ↑m ω ) ∈ V ) |
7 |
|
fvex |
⊢ ( 𝑆 ‘ 𝑁 ) ∈ V |
8 |
|
unab |
⊢ ( { 𝑥 ∣ ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) } ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) } ) = { 𝑥 ∣ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } |
9 |
7
|
abrexex |
⊢ { 𝑥 ∣ ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) } ∈ V |
10 |
|
simpl |
⊢ ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) → 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) |
11 |
10
|
reximi |
⊢ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) → ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ) |
12 |
11
|
ss2abi |
⊢ { 𝑥 ∣ ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) } ⊆ { 𝑥 ∣ ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) } |
13 |
9 12
|
ssexi |
⊢ { 𝑥 ∣ ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) } ∈ V |
14 |
|
omex |
⊢ ω ∈ V |
15 |
14
|
abrexex |
⊢ { 𝑥 ∣ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) } ∈ V |
16 |
|
simpl |
⊢ ( ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) → 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) |
17 |
16
|
reximi |
⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) → ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ) |
18 |
17
|
ss2abi |
⊢ { 𝑥 ∣ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) } ⊆ { 𝑥 ∣ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) } |
19 |
15 18
|
ssexi |
⊢ { 𝑥 ∣ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) } ∈ V |
20 |
13 19
|
unex |
⊢ ( { 𝑥 ∣ ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) } ∪ { 𝑥 ∣ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) } ) ∈ V |
21 |
8 20
|
eqeltrri |
⊢ { 𝑥 ∣ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ∈ V |
22 |
21
|
a1i |
⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ) ∧ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ) → { 𝑥 ∣ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ∈ V ) |
23 |
22
|
ralrimiva |
⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ) → ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) { 𝑥 ∣ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ∈ V ) |
24 |
|
abrexex2g |
⊢ ( ( ( 𝑆 ‘ 𝑁 ) ∈ V ∧ ∀ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) { 𝑥 ∣ ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ∈ V ) → { 𝑥 ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ∈ V ) |
25 |
7 23 24
|
sylancr |
⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) ∧ 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ) → { 𝑥 ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ∈ V ) |
26 |
6 25
|
opabex3rd |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ∧ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ) } ∈ V ) |
27 |
3 26
|
eqeltrid |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → { 〈 𝑥 , 𝑦 〉 ∣ ( ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑁 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { 〈 𝑖 , 𝑧 〉 } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) ∧ 𝑦 ∈ 𝒫 ( 𝑀 ↑m ω ) ) } ∈ V ) |