satffunlem1lem2

		Ref	Expression
	Assertion	satffunlem1lem2	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		peano1	⊢ ∅ ∈ ω
2		satfdmfmla	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = ( Fmla ‘ ∅ ) )
3	1 2	mp3an3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = ( Fmla ‘ ∅ ) )
4		ovex	⊢ ( 𝑀 ↑_m ω ) ∈ V
5	4	difexi	⊢ ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ∈ V
6	5	a1i	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ∈ V )
7	6	ralrimiva	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ∀ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ∈ V )
8	4	rabex	⊢ { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ∈ V
9	8	a1i	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑖 ∈ ω ) → { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ∈ V )
10	9	ralrimiva	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ∀ 𝑖 ∈ ω { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ∈ V )
11	7 10	jca	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( ∀ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ∈ V ∧ ∀ 𝑖 ∈ ω { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ∈ V ) )
12	11	ralrimiva	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ∀ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∀ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ∈ V ∧ ∀ 𝑖 ∈ ω { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ∈ V ) )
13		dmopab2rex	⊢ ( ∀ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∀ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ∈ V ∧ ∀ 𝑖 ∈ ω { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ∈ V ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } )
14	12 13	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } )
15		satfrel	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
16	1 15	mp3an3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
17		1stdm	⊢ ( ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
18	16 17	sylan	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
19	2	eqcomd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω ) → ( Fmla ‘ ∅ ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
20	1 19	mp3an3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Fmla ‘ ∅ ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
21	20	adantr	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( Fmla ‘ ∅ ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
22	18 21	eleqtrrd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( 1^st ‘ 𝑢 ) ∈ ( Fmla ‘ ∅ ) )
23	22	adantr	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) → ( 1^st ‘ 𝑢 ) ∈ ( Fmla ‘ ∅ ) )
24		oveq1	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → ( 𝑓 ⊼_𝑔 𝑔 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) )
25	24	eqeq2d	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → ( 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ↔ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) )
26	25	rexbidv	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ↔ ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) )
27		eqidd	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → 𝑖 = 𝑖 )
28		id	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → 𝑓 = ( 1^st ‘ 𝑢 ) )
29	27 28	goaleq12d	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → ∀_𝑔 𝑖 𝑓 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) )
30	29	eqeq2d	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → ( 𝑥 = ∀_𝑔 𝑖 𝑓 ↔ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) )
31	30	rexbidv	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) )
32	26 31	orbi12d	⊢ ( 𝑓 = ( 1^st ‘ 𝑢 ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ↔ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
33	32	adantl	⊢ ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑢 ) ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ↔ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
34		1stdm	⊢ ( ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
35	16 34	sylan	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
36	20	adantr	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( Fmla ‘ ∅ ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
37	35 36	eleqtrrd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( 1^st ‘ 𝑣 ) ∈ ( Fmla ‘ ∅ ) )
38	37	ad4ant13	⊢ ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) → ( 1^st ‘ 𝑣 ) ∈ ( Fmla ‘ ∅ ) )
39		oveq2	⊢ ( 𝑔 = ( 1^st ‘ 𝑣 ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) )
40	39	eqeq2d	⊢ ( 𝑔 = ( 1^st ‘ 𝑣 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ↔ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
41	40	adantl	⊢ ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) ∧ 𝑔 = ( 1^st ‘ 𝑣 ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ↔ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
42		simpr	⊢ ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) → 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) )
43	38 41 42	rspcedvd	⊢ ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) → ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) )
44	43	ex	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) )
45	44	rexlimdva	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) )
46	45	orim1d	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
47	46	imp	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) → ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) )
48	23 33 47	rspcedvd	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) → ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) )
49	48	ex	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) )
50	49	rexlimdva	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) )
51		releldm2	⊢ ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) → ( 𝑓 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑢 ) = 𝑓 ) )
52	16 51	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑓 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑢 ) = 𝑓 ) )
53	3	eleq2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑓 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ 𝑓 ∈ ( Fmla ‘ ∅ ) ) )
54	52 53	bitr3d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑢 ) = 𝑓 ↔ 𝑓 ∈ ( Fmla ‘ ∅ ) ) )
55		r19.41v	⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ( 1^st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) ↔ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) )
56		oveq1	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) = ( 𝑓 ⊼_𝑔 𝑔 ) )
57	56	eqeq2d	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ↔ 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ) )
58	57	rexbidv	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ↔ ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ) )
59		eqidd	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → 𝑖 = 𝑖 )
60		id	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → ( 1^st ‘ 𝑢 ) = 𝑓 )
61	59 60	goaleq12d	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑖 𝑓 )
62	61	eqeq2d	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ 𝑥 = ∀_𝑔 𝑖 𝑓 ) )
63	62	rexbidv	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) )
64	58 63	orbi12d	⊢ ( ( 1^st ‘ 𝑢 ) = 𝑓 → ( ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) )
65	64	adantl	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ ( 1^st ‘ 𝑢 ) = 𝑓 ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) )
66	3	eqcomd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Fmla ‘ ∅ ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
67	66	eleq2d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑔 ∈ ( Fmla ‘ ∅ ) ↔ 𝑔 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) )
68		releldm2	⊢ ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) → ( 𝑔 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑣 ) = 𝑔 ) )
69	16 68	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑔 ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑣 ) = 𝑔 ) )
70	67 69	bitrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑔 ∈ ( Fmla ‘ ∅ ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑣 ) = 𝑔 ) )
71		r19.41v	⊢ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ( 1^st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) ↔ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) )
72	39	eqcoms	⊢ ( ( 1^st ‘ 𝑣 ) = 𝑔 → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) )
73	72	eqeq2d	⊢ ( ( 1^st ‘ 𝑣 ) = 𝑔 → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ↔ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
74	73	biimpa	⊢ ( ( ( 1^st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) → 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) )
75	74	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 1^st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) → 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
76	75	reximdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ( 1^st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) → ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
77	71 76	biimtrrid	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑣 ) = 𝑔 ∧ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ) → ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
78	77	expd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑣 ) = 𝑔 → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) ) )
79	70 78	sylbid	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑔 ∈ ( Fmla ‘ ∅ ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) ) )
80	79	rexlimdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
81	80	adantr	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
82	81	adantr	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ ( 1^st ‘ 𝑢 ) = 𝑓 ) → ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) → ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
83	82	orim1d	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ ( 1^st ‘ 𝑢 ) = 𝑓 ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
84	65 83	sylbird	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ∧ ( 1^st ‘ 𝑢 ) = 𝑓 ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
85	84	expimpd	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) → ( ( ( 1^st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
86	85	reximdva	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ( 1^st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) → ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
87	55 86	biimtrrid	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑢 ) = 𝑓 ∧ ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) → ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
88	87	expd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 1^st ‘ 𝑢 ) = 𝑓 → ( ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) → ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) )
89	54 88	sylbird	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑓 ∈ ( Fmla ‘ ∅ ) → ( ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) → ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) ) )
90	89	rexlimdv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) → ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
91	50 90	impbid	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ↔ ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) ) )
92	91	abbidv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → { 𝑥 ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) } = { 𝑥 ∣ ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) } )
93	14 92	eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } = { 𝑥 ∣ ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) } )
94	3 93	ineq12d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) = ( ( Fmla ‘ ∅ ) ∩ { 𝑥 ∣ ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) } ) )
95		fmla0disjsuc	⊢ ( ( Fmla ‘ ∅ ) ∩ { 𝑥 ∣ ∃ 𝑓 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑔 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑓 ⊼_𝑔 𝑔 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 𝑓 ) } ) = ∅
96	94 95	eqtrdi	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∩ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑗 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑗 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) = ∅ )

Metamath Proof Explorer

Theorem satffunlem1lem2

Proof