satfdmlem

		Ref	Expression
	Assertion	satfdmlem	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		satfrel	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) )
2	1	adantr	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) )
3		1stdm	⊢ ( ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) )
4	2 3	sylan	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) )
5		eleq2	⊢ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) → ( ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ↔ ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) )
6	5	adantl	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → ( ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ↔ ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) )
7	6	adantr	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ↔ ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) )
8		fvex	⊢ ( 1^st ‘ 𝑢 ) ∈ V
9		eldm2g	⊢ ( ( 1^st ‘ 𝑢 ) ∈ V → ( ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ↔ ∃ 𝑠 ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) )
10	8 9	ax-mp	⊢ ( ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ↔ ∃ 𝑠 ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) )
11		simpr	⊢ ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) )
12	2	ad4antr	⊢ ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) )
13		1stdm	⊢ ( ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) )
14	12 13	sylancom	⊢ ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) )
15		eleq2	⊢ ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) → ( ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ↔ ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) )
16	15	ad5antlr	⊢ ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ↔ ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) )
17		fvex	⊢ ( 1^st ‘ 𝑣 ) ∈ V
18		eldm2g	⊢ ( ( 1^st ‘ 𝑣 ) ∈ V → ( ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ↔ ∃ 𝑟 ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) )
19	17 18	ax-mp	⊢ ( ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ↔ ∃ 𝑟 ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) )
20		simpr	⊢ ( ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) )
21		vex	⊢ 𝑠 ∈ V
22	8 21	op1std	⊢ ( 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ → ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑢 ) )
23	22	eqcomd	⊢ ( 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑎 ) )
24	23	ad3antlr	⊢ ( ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ 𝑎 ) )
25		vex	⊢ 𝑟 ∈ V
26	17 25	op1std	⊢ ( 𝑏 = ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ → ( 1^st ‘ 𝑏 ) = ( 1^st ‘ 𝑣 ) )
27	26	eqcomd	⊢ ( 𝑏 = ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ → ( 1^st ‘ 𝑣 ) = ( 1^st ‘ 𝑏 ) )
28	24 27	oveqan12d	⊢ ( ( ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑏 = ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ) → ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) )
29	28	eqeq2d	⊢ ( ( ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑏 = ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ↔ 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) )
30	29	biimpd	⊢ ( ( ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑏 = ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) )
31	20 30	rspcimedv	⊢ ( ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) )
32	31	ex	⊢ ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) ) )
33	32	exlimdv	⊢ ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ∃ 𝑟 ⟨ ( 1^st ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) ) )
34	19 33	syl5bi	⊢ ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) ) )
35	16 34	sylbid	⊢ ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ( 1^st ‘ 𝑣 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) ) )
36	14 35	mpd	⊢ ( ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) ∧ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) )
37	36	rexlimdva	⊢ ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) → ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) → ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ) )
38		eqidd	⊢ ( 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ → 𝑖 = 𝑖 )
39	38 23	goaleq12d	⊢ ( 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ → ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) )
40	39	eqeq2d	⊢ ( 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ↔ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) )
41	40	biimpd	⊢ ( 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) )
42	41	adantl	⊢ ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) → ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) )
43	42	reximdv	⊢ ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) → ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) → ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) )
44	37 43	orim12d	⊢ ( ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑎 = ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) )
45	11 44	rspcimedv	⊢ ( ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) ∧ ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) )
46	45	ex	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) ) )
47	46	exlimdv	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ∃ 𝑠 ⟨ ( 1^st ‘ 𝑢 ) , 𝑠 ⟩ ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) ) )
48	10 47	syl5bi	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) ) )
49	7 48	sylbid	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ( 1^st ‘ 𝑢 ) ∈ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) ) )
50	4 49	mpd	⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) ∧ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ) → ( ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) )
51	50	rexlimdva	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑌 ∈ ω ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) = dom ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ) → ( ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) → ∃ 𝑎 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) ( ∃ 𝑏 ∈ ( ( 𝑁 Sat 𝐹 ) ‘ 𝑌 ) 𝑥 = ( ( 1^st ‘ 𝑎 ) ⊼_𝑔 ( 1^st ‘ 𝑏 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑎 ) ) ) )

Metamath Proof Explorer

Theorem satfdmlem

Proof