satfvsuclem1

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

Proof

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

Metamath Proof Explorer

Theorem satfvsuclem1

Proof