Metamath Proof Explorer


Theorem satfvsuclem1

Description: Lemma 1 for satfvsuc . (Contributed by AV, 8-Oct-2023)

Ref Expression
Hypothesis satfv0.s 𝑆 = ( 𝑀 Sat 𝐸 )
Assertion satfvsuclem1 ( ( 𝑀𝑉𝐸𝑊𝑁 ∈ ω ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ∃ 𝑢 ∈ ( 𝑆𝑁 ) ( ∃ 𝑣 ∈ ( 𝑆𝑁 ) ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀m ω ) ∣ ∀ 𝑧𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd𝑢 ) } ) ) ∧ 𝑦 ∈ 𝒫 ( 𝑀m ω ) ) } ∈ V )

Proof

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 )