satffunlem1lem1

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

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑢 = 𝑠 → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) )
2		fveq2	⊢ ( 𝑣 = 𝑟 → ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑟 ) )
3	1 2	oveqan12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) )
4	3	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ) )
5		fveq2	⊢ ( 𝑢 = 𝑠 → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
6		fveq2	⊢ ( 𝑣 = 𝑟 → ( 2^nd ‘ 𝑣 ) = ( 2^nd ‘ 𝑟 ) )
7	5 6	ineqan12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) = ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) )
8	7	difeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) )
9	8	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ↔ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) )
10	4 9	anbi12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑣 = 𝑟 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) )
11	10	cbvrexdva	⊢ ( 𝑢 = 𝑠 → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) )
12		simpr	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → 𝑖 = 𝑗 )
13	1	adantr	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) )
14	12 13	goaleq12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) )
15	14	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ) )
16		opeq1	⊢ ( 𝑖 = 𝑗 → ⟨ 𝑖 , 𝑘 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
17	16	sneqd	⊢ ( 𝑖 = 𝑗 → { ⟨ 𝑖 , 𝑘 ⟩ } = { ⟨ 𝑗 , 𝑘 ⟩ } )
18		sneq	⊢ ( 𝑖 = 𝑗 → { 𝑖 } = { 𝑗 } )
19	18	difeq2d	⊢ ( 𝑖 = 𝑗 → ( ω ∖ { 𝑖 } ) = ( ω ∖ { 𝑗 } ) )
20	19	reseq2d	⊢ ( 𝑖 = 𝑗 → ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) = ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) )
21	17 20	uneq12d	⊢ ( 𝑖 = 𝑗 → ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) = ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) )
22	21	adantl	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) = ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) )
23	5	adantr	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
24	22 23	eleq12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) ↔ ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) ) )
25	24	ralbidv	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) ↔ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) ) )
26	25	rabbidv	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } )
27	26	eqeq2d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ↔ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) )
28	15 27	anbi12d	⊢ ( ( 𝑢 = 𝑠 ∧ 𝑖 = 𝑗 ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) )
29	28	cbvrexdva	⊢ ( 𝑢 = 𝑠 → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) )
30	11 29	orbi12d	⊢ ( 𝑢 = 𝑠 → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) ) )
31	30	cbvrexvw	⊢ ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) )
32		simp-4l	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
33		simpr	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
34	33	anim1i	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
35		simpr	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
36	35	anim1i	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
37	36	ad2antrr	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
38		satffunlem	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ ( 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) → 𝑧 = 𝑦 )
39	38	eqcomd	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ ( 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∧ ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ) → 𝑦 = 𝑧 )
40	39	3exp	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ ( 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) ) )
41	32 34 37 40	syl3anc	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) ) )
42	41	rexlimdva	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) ) )
43		eqeq1	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ↔ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ) )
44		df-goal	⊢ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩
45		fvex	⊢ ( 1^st ‘ 𝑠 ) ∈ V
46		fvex	⊢ ( 1^st ‘ 𝑟 ) ∈ V
47		gonafv	⊢ ( ( ( 1^st ‘ 𝑠 ) ∈ V ∧ ( 1^st ‘ 𝑟 ) ∈ V ) → ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ )
48	45 46 47	mp2an	⊢ ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩
49	44 48	eqeq12i	⊢ ( ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ↔ ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ )
50		2oex	⊢ 2_o ∈ V
51		opex	⊢ ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ∈ V
52	50 51	opth	⊢ ( ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ ↔ ( 2_o = 1_o ∧ ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ = ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ) )
53		1one2o	⊢ 1_o ≠ 2_o
54		df-ne	⊢ ( 1_o ≠ 2_o ↔ ¬ 1_o = 2_o )
55		pm2.21	⊢ ( ¬ 1_o = 2_o → ( 1_o = 2_o → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → 𝑦 = 𝑧 ) ) )
56	54 55	sylbi	⊢ ( 1_o ≠ 2_o → ( 1_o = 2_o → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → 𝑦 = 𝑧 ) ) )
57	53 56	ax-mp	⊢ ( 1_o = 2_o → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → 𝑦 = 𝑧 ) )
58	57	eqcoms	⊢ ( 2_o = 1_o → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → 𝑦 = 𝑧 ) )
59	58	adantr	⊢ ( ( 2_o = 1_o ∧ ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ = ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → 𝑦 = 𝑧 ) )
60	52 59	sylbi	⊢ ( ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑠 ) , ( 1^st ‘ 𝑟 ) ⟩ ⟩ → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → 𝑦 = 𝑧 ) )
61	49 60	sylbi	⊢ ( ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → 𝑦 = 𝑧 ) )
62	43 61	biimtrdi	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) → 𝑦 = 𝑧 ) ) )
63	62	impd	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) )
64	63	adantr	⊢ ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) )
65	64	a1i	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑖 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) ) )
66	65	rexlimdva	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) ) )
67	42 66	jaod	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) ) )
68	67	rexlimdva	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → 𝑦 = 𝑧 ) ) )
69	68	com23	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑦 = 𝑧 ) ) )
70	69	rexlimdva	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ∃ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑦 = 𝑧 ) ) )
71		eqeq1	⊢ ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ) )
72		df-goal	⊢ ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) = ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩
73		fvex	⊢ ( 1^st ‘ 𝑢 ) ∈ V
74		fvex	⊢ ( 1^st ‘ 𝑣 ) ∈ V
75		gonafv	⊢ ( ( ( 1^st ‘ 𝑢 ) ∈ V ∧ ( 1^st ‘ 𝑣 ) ∈ V ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ )
76	73 74 75	mp2an	⊢ ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩
77	72 76	eqeq12i	⊢ ( ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ )
78		opex	⊢ ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ∈ V
79	50 78	opth	⊢ ( ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ ↔ ( 2_o = 1_o ∧ ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ = ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ) )
80		pm2.21	⊢ ( ¬ 1_o = 2_o → ( 1_o = 2_o → 𝑦 = 𝑧 ) )
81	54 80	sylbi	⊢ ( 1_o ≠ 2_o → ( 1_o = 2_o → 𝑦 = 𝑧 ) )
82	53 81	ax-mp	⊢ ( 1_o = 2_o → 𝑦 = 𝑧 )
83	82	eqcoms	⊢ ( 2_o = 1_o → 𝑦 = 𝑧 )
84	83	adantr	⊢ ( ( 2_o = 1_o ∧ ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ = ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ) → 𝑦 = 𝑧 )
85	79 84	sylbi	⊢ ( ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ = ⟨ 1_o , ⟨ ( 1^st ‘ 𝑢 ) , ( 1^st ‘ 𝑣 ) ⟩ ⟩ → 𝑦 = 𝑧 )
86	77 85	sylbi	⊢ ( ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → 𝑦 = 𝑧 )
87	71 86	biimtrdi	⊢ ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → 𝑦 = 𝑧 ) )
88	87	adantr	⊢ ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → 𝑦 = 𝑧 ) )
89	88	com12	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) )
90	89	adantr	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) )
91	90	a1i	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) ) )
92	91	rexlimdva	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) ) )
93		eqeq1	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ) )
94	44 72	eqeq12i	⊢ ( ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ = ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ )
95	50 51	opth	⊢ ( ⟨ 2_o , ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ ⟩ = ⟨ 2_o , ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ⟩ ↔ ( 2_o = 2_o ∧ ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ = ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ) )
96		vex	⊢ 𝑖 ∈ V
97	96 73	opth	⊢ ( ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ = ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ↔ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) )
98	97	anbi2i	⊢ ( ( 2_o = 2_o ∧ ⟨ 𝑖 , ( 1^st ‘ 𝑢 ) ⟩ = ⟨ 𝑗 , ( 1^st ‘ 𝑠 ) ⟩ ) ↔ ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) )
99	94 95 98	3bitri	⊢ ( ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) )
100	93 99	bitrdi	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) ) )
101	100	adantl	⊢ ( ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑖 ∈ ω ) ∧ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ↔ ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) ) )
102		funfv1st2nd	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) )
103	102	ex	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ) )
104		funfv1st2nd	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) )
105	104	ex	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ) )
106		fveqeq2	⊢ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) ↔ ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑢 ) ) )
107		eqtr2	⊢ ( ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
108		opeq1	⊢ ( 𝑗 = 𝑖 → ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑖 , 𝑘 ⟩ )
109	108	sneqd	⊢ ( 𝑗 = 𝑖 → { ⟨ 𝑗 , 𝑘 ⟩ } = { ⟨ 𝑖 , 𝑘 ⟩ } )
110		sneq	⊢ ( 𝑗 = 𝑖 → { 𝑗 } = { 𝑖 } )
111	110	difeq2d	⊢ ( 𝑗 = 𝑖 → ( ω ∖ { 𝑗 } ) = ( ω ∖ { 𝑖 } ) )
112	111	reseq2d	⊢ ( 𝑗 = 𝑖 → ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) = ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) )
113	109 112	uneq12d	⊢ ( 𝑗 = 𝑖 → ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) = ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) )
114	113	eqcoms	⊢ ( 𝑖 = 𝑗 → ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) = ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) )
115	114	adantl	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) = ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) )
116		simpl	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) )
117	116	eqcomd	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( 2^nd ‘ 𝑠 ) = ( 2^nd ‘ 𝑢 ) )
118	115 117	eleq12d	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) ↔ ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) ) )
119	118	ralbidv	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) ↔ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) ) )
120	119	rabbidv	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } )
121		eqeq12	⊢ ( ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → ( 𝑦 = 𝑧 ↔ { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) )
122	120 121	syl5ibrcom	⊢ ( ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → 𝑦 = 𝑧 ) )
123	122	exp4b	⊢ ( ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ 𝑠 ) → ( 𝑖 = 𝑗 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) )
124	107 123	syl	⊢ ( ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑢 ) ∧ ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) ) → ( 𝑖 = 𝑗 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) )
125	124	ex	⊢ ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑢 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( 𝑖 = 𝑗 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) )
126	106 125	biimtrdi	⊢ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( 𝑖 = 𝑗 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) ) )
127	126	com24	⊢ ( ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) → ( 𝑖 = 𝑗 → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) ) )
128	127	impcom	⊢ ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) )
129	128	com13	⊢ ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ 𝑢 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) )
130	105 129	syl6	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) ) )
131	130	com23	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ‘ ( 1^st ‘ 𝑠 ) ) = ( 2^nd ‘ 𝑠 ) → ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) ) )
132	103 131	syld	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) ) )
133	132	imp	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) )
134	133	adantr	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) → ( 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) ) )
135	134	imp	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) )
136	135	adantld	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) )
137	136	ad2antrr	⊢ ( ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑖 ∈ ω ) ∧ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ( 2_o = 2_o ∧ ( 𝑖 = 𝑗 ∧ ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑠 ) ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) )
138	101 137	sylbid	⊢ ( ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑖 ∈ ω ) ∧ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) )
139	138	impd	⊢ ( ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑖 ∈ ω ) ∧ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) )
140	139	ex	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑖 ∈ ω ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → 𝑦 = 𝑧 ) ) ) )
141	140	com34	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑖 ∈ ω ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) ) ) )
142	141	impd	⊢ ( ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑖 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) ) )
143	142	rexlimdva	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) ) )
144	92 143	jaod	⊢ ( ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) ) )
145	144	rexlimdva	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → 𝑦 = 𝑧 ) ) )
146	145	com23	⊢ ( ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ω ) → ( ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑦 = 𝑧 ) ) )
147	146	rexlimdva	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑦 = 𝑧 ) ) )
148	70 147	jaod	⊢ ( ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) → ( ( ∃ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑦 = 𝑧 ) ) )
149	148	rexlimdva	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ∃ 𝑠 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑟 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑠 ) ⊼_𝑔 ( 1^st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑠 ) ∩ ( 2^nd ‘ 𝑟 ) ) ) ) ∨ ∃ 𝑗 ∈ ω ( 𝑥 = ∀_𝑔 𝑗 ( 1^st ‘ 𝑠 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑗 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑗 } ) ) ) ∈ ( 2^nd ‘ 𝑠 ) } ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑦 = 𝑧 ) ) )
150	31 149	biimtrid	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) → 𝑦 = 𝑧 ) ) )
151	150	impd	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ( ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∧ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) → 𝑦 = 𝑧 ) )
152	151	alrimivv	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∧ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) → 𝑦 = 𝑧 ) )
153		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ↔ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) )
154	153	anbi2d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) )
155	154	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ) )
156		eqeq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ↔ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) )
157	156	anbi2d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
158	157	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
159	155 158	orbi12d	⊢ ( 𝑦 = 𝑧 → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
160	159	rexbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) )
161	160	mo4	⊢ ( ∃* 𝑦 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ∧ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑧 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ) → 𝑦 = 𝑧 ) )
162	152 161	sylibr	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ∃* 𝑦 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
163	162	alrimiv	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → ∀ 𝑥 ∃* 𝑦 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
164		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ↔ ∀ 𝑥 ∃* 𝑦 ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) )
165	163 164	sylibr	⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑓 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } )

Metamath Proof Explorer

Theorem satffunlem1lem1

Proof