satffunlem1lem1 - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > satffunlem1lem1		Structured version Visualization version GIF version

Theorem satffunlem1lem1 32649

Description: Lemma for satffunlem1 32654. (Contributed by AV, 17-Oct-2023.)

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

Distinct variable groups: 𝑖,𝐸,𝑢,𝑥,𝑦 𝑣,𝐸,𝑢,𝑥,𝑦 𝑖,𝑀,𝑢,𝑥,𝑦 𝑣,𝑀 𝑖,𝑁,𝑢,𝑥,𝑦 𝑣,𝑁 𝑓,𝑖,𝑢,𝑦 𝑣,𝑓 𝑖,𝑘,𝑢,𝑦 𝑣,𝑘 Allowed substitution hints: 𝐸(𝑓,𝑘) 𝑀(𝑓,𝑘) 𝑁(𝑓,𝑘)

Proof of Theorem satffunlem1lem1 Dummy variables 𝑗 𝑠 𝑧 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑠 → (1^st ‘𝑢) = (1^st ‘𝑠))
2		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑟 → (1^st ‘𝑣) = (1^st ‘𝑟))
3	1, 2	oveqan12d 7175	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)))
4	3	eqeq2d 2832	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ↔ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))))
5		fveq2 6670	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑠 → (2^nd ‘𝑢) = (2^nd ‘𝑠))
6		fveq2 6670	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑟 → (2^nd ‘𝑣) = (2^nd ‘𝑟))
7	5, 6	ineqan12d 4191	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)) = ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))
8	7	difeq2d 4099	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))
9	8	eqeq2d 2832	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))))
10	4, 9	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))))
11	10	cbvrexdva 3460	. . . . . . . . 9 ⊢ (𝑢 = 𝑠 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ ∃𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))))
12		simpr 487	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
13	1	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (1^st ‘𝑢) = (1^st ‘𝑠))
14	12, 13	goaleq12d 32598	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑗(1^st ‘𝑠))
15	14	eqeq2d 2832	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ 𝑥 = ∀_𝑔𝑗(1^st ‘𝑠)))
16		opeq1 4803	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ⟨𝑖, 𝑘⟩ = ⟨𝑗, 𝑘⟩)
17	16	sneqd 4579	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → {⟨𝑖, 𝑘⟩} = {⟨𝑗, 𝑘⟩})
18		sneq 4577	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → {𝑖} = {𝑗})
19	18	difeq2d 4099	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (ω ∖ {𝑖}) = (ω ∖ {𝑗}))
20	19	reseq2d 5853	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → (𝑓 ↾ (ω ∖ {𝑖})) = (𝑓 ↾ (ω ∖ {𝑗})))
21	17, 20	uneq12d 4140	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑗 → ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) = ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))))
22	21	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) = ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))))
23	5	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (2^nd ‘𝑢) = (2^nd ‘𝑠))
24	22, 23	eleq12d 2907	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢) ↔ ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)))
25	24	ralbidv 3197	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢) ↔ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)))
26	25	rabbidv 3480	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})
27	26	eqeq2d 2832	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ↔ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}))
28	15, 27	anbi12d 632	. . . . . . . . . 10 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})))
29	28	cbvrexdva 3460	. . . . . . . . 9 ⊢ (𝑢 = 𝑠 → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ ∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})))
30	11, 29	orbi12d 915	. . . . . . . 8 ⊢ (𝑢 = 𝑠 → ((∃𝑣 ∈ ((𝑀 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 3450	. . . . . . 7 ⊢ (∃𝑢 ∈ ((𝑀 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 781	. . . . . . . . . . . . . . 15 ⊢ (((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → Fun ((𝑀 Sat 𝐸)‘𝑁))
33		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ ((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁))
34	33	anim1i 616	. . . . . . . . . . . . . . 15 ⊢ (((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)))
35		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁))
36	35	anim1i 616	. . . . . . . . . . . . . . . 16 ⊢ (((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)))
37	36	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)))
38		satffunlem 32648	. . . . . . . . . . . . . . . . 17 ⊢ (((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 2827	. . . . . . . . . . . . . . . 16 ⊢ (((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 1115	. . . . . . . . . . . . . . 15 ⊢ ((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 1367	. . . . . . . . . . . . . 14 ⊢ (((((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 3284	. . . . . . . . . . . . 13 ⊢ ((((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 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ ∀_𝑔𝑖(1^st ‘𝑢) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))))
44		df-goal 32589	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀_𝑔𝑖(1^st ‘𝑢) = ⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩
45		fvex 6683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘𝑠) ∈ V
46		fvex 6683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1^st ‘𝑟) ∈ V
47		gonafv 32597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1^st ‘𝑠) ∈ V ∧ (1^st ‘𝑟) ∈ V) → ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
48	45, 46, 47	mp2an 690	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩
49	44, 48	eqeq12i 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀_𝑔𝑖(1^st ‘𝑢) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ↔ ⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
50		2oex 8112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2_o ∈ V
51		opex 5356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑖, (1^st ‘𝑢)⟩ ∈ V
52	50, 51	opth 5368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩ ↔ (2_o = 1_o ∧ ⟨𝑖, (1^st ‘𝑢)⟩ = ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩))
53		1one2o 8269	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1_o ≠ 2_o
54		df-ne 3017	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1_o ≠ 2_o ↔ ¬ 1_o = 2_o)
55		pm2.21 123	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 1_o = 2_o → (1_o = 2_o → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → 𝑦 = 𝑧)))
56	54, 55	sylbi 219	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1_o ≠ 2_o → (1_o = 2_o → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → 𝑦 = 𝑧)))
57	53, 56	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1_o = 2_o → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → 𝑦 = 𝑧))
58	57	eqcoms 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2_o = 1_o → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → 𝑦 = 𝑧))
59	58	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2_o = 1_o ∧ ⟨𝑖, (1^st ‘𝑢)⟩ = ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → 𝑦 = 𝑧))
60	52, 59	sylbi 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → 𝑦 = 𝑧))
61	49, 60	sylbi 219	. . . . . . . . . . . . . . . . . 18 ⊢ (∀_𝑔𝑖(1^st ‘𝑢) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → 𝑦 = 𝑧))
62	43, 61	syl6bi 255	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))) → 𝑦 = 𝑧)))
63	62	impd 413	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑧))
64	63	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑧))
65	64	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑧)))
66	65	rexlimdva 3284	. . . . . . . . . . . . 13 ⊢ ((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑧)))
67	42, 66	jaod 855	. . . . . . . . . . . 12 ⊢ ((((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 3284	. . . . . . . . . . 11 ⊢ (((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 86	. . . . . . . . . 10 ⊢ (((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 3284	. . . . . . . . 9 ⊢ ((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 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ↔ ∀_𝑔𝑗(1^st ‘𝑠) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
72		df-goal 32589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀_𝑔𝑗(1^st ‘𝑠) = ⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩
73		fvex 6683	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1^st ‘𝑢) ∈ V
74		fvex 6683	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1^st ‘𝑣) ∈ V
75		gonafv 32597	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑢) ∈ V ∧ (1^st ‘𝑣) ∈ V) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩)
76	73, 74, 75	mp2an 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩
77	72, 76	eqeq12i 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀_𝑔𝑗(1^st ‘𝑠) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ↔ ⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩)
78		opex 5356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ⟨𝑗, (1^st ‘𝑠)⟩ ∈ V
79	50, 78	opth 5368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ ↔ (2_o = 1_o ∧ ⟨𝑗, (1^st ‘𝑠)⟩ = ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩))
80		pm2.21 123	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 1_o = 2_o → (1_o = 2_o → 𝑦 = 𝑧))
81	54, 80	sylbi 219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1_o ≠ 2_o → (1_o = 2_o → 𝑦 = 𝑧))
82	53, 81	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1_o = 2_o → 𝑦 = 𝑧)
83	82	eqcoms 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2_o = 1_o → 𝑦 = 𝑧)
84	83	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2_o = 1_o ∧ ⟨𝑗, (1^st ‘𝑠)⟩ = ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩) → 𝑦 = 𝑧)
85	79, 84	sylbi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ → 𝑦 = 𝑧)
86	77, 85	sylbi 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀_𝑔𝑗(1^st ‘𝑠) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → 𝑦 = 𝑧)
87	71, 86	syl6bi 255	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → 𝑦 = 𝑧))
88	87	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → 𝑦 = 𝑧))
89	88	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑧))
90	89	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑧 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑧))
91	90	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑧 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑧)))
92	91	rexlimdva 3284	. . . . . . . . . . . . 13 ⊢ ((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑧 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑧)))
93		eqeq1 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ↔ ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑗(1^st ‘𝑠)))
94	44, 72	eqeq12i 2836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑗(1^st ‘𝑠) ↔ ⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ = ⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩)
95	50, 51	opth 5368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ = ⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩ ↔ (2_o = 2_o ∧ ⟨𝑖, (1^st ‘𝑢)⟩ = ⟨𝑗, (1^st ‘𝑠)⟩))
96		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑖 ∈ V
97	96, 73	opth 5368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑖, (1^st ‘𝑢)⟩ = ⟨𝑗, (1^st ‘𝑠)⟩ ↔ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)))
98	97	anbi2i 624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2_o = 2_o ∧ ⟨𝑖, (1^st ‘𝑢)⟩ = ⟨𝑗, (1^st ‘𝑠)⟩) ↔ (2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠))))
99	94, 95, 98	3bitri 299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑗(1^st ‘𝑠) ↔ (2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠))))
100	93, 99	syl6bb 289	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ↔ (2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)))))
101	100	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ↔ (2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)))))
102		funfv1st2nd 7745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠))
103	102	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) → (((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠)))
104		funfv1st2nd 7745	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢))
105	104	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → (((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢)))
106		fveqeq2 6679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ↔ (((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑢)))
107		eqtr2 2842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑢) ∧ (((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠)) → (2^nd ‘𝑢) = (2^nd ‘𝑠))
108		opeq1 4803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑗 = 𝑖 → ⟨𝑗, 𝑘⟩ = ⟨𝑖, 𝑘⟩)
109	108	sneqd 4579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑗 = 𝑖 → {⟨𝑗, 𝑘⟩} = {⟨𝑖, 𝑘⟩})
110		sneq 4577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑗 = 𝑖 → {𝑗} = {𝑖})
111	110	difeq2d 4099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑗 = 𝑖 → (ω ∖ {𝑗}) = (ω ∖ {𝑖}))
112	111	reseq2d 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑗 = 𝑖 → (𝑓 ↾ (ω ∖ {𝑗})) = (𝑓 ↾ (ω ∖ {𝑖})))
113	109, 112	uneq12d 4140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑗 = 𝑖 → ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))))
114	113	eqcoms 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑖 = 𝑗 → ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))))
115	114	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))))
116		simpl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → (2^nd ‘𝑢) = (2^nd ‘𝑠))
117	116	eqcomd 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → (2^nd ‘𝑠) = (2^nd ‘𝑢))
118	115, 117	eleq12d 2907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → (({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠) ↔ ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)))
119	118	ralbidv 3197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → (∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠) ↔ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)))
120	119	rabbidv 3480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})
121		eqeq12 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → (𝑦 = 𝑧 ↔ {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))
122	120, 121	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → ((𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → 𝑦 = 𝑧))
123	122	exp4b 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((2^nd ‘𝑢) = (2^nd ‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))
124	107, 123	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑢) ∧ (((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠)) → (𝑖 = 𝑗 → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))
125	124	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑢) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧)))))
126	106, 125	syl6bi 255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))))
127	126	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → (𝑖 = 𝑗 → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))))
128	127	impcom 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧)))))
129	128	com13 88	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧)))))
130	105, 129	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))))
131	130	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))))
132	103, 131	syld 47	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))))
133	132	imp 409	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧)))))
134	133	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧)))))
135	134	imp 409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))
136	135	adantld 493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠))) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))
137	136	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ((2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠))) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))
138	101, 137	sylbid 242	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))
139	138	impd 413	. . . . . . . . . . . . . . . . 17 ⊢ ((((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧)))
140	139	ex 415	. . . . . . . . . . . . . . . 16 ⊢ (((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 = 𝑧))))
141	140	com34 91	. . . . . . . . . . . . . . 15 ⊢ (((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → (𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑧))))
142	141	impd 413	. . . . . . . . . . . . . 14 ⊢ (((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑧)))
143	142	rexlimdva 3284	. . . . . . . . . . . . 13 ⊢ ((((Fun ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑗, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑧)))
144	92, 143	jaod 855	. . . . . . . . . . . 12 ⊢ ((((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 3284	. . . . . . . . . . 11 ⊢ (((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 86	. . . . . . . . . 10 ⊢ (((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 3284	. . . . . . . . 9 ⊢ ((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 855	. . . . . . . 8 ⊢ ((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 3284	. . . . . . 7 ⊢ (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	syl5bi 244	. . . . . 6 ⊢ (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 413	. . . . 5 ⊢ (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 1929	. . . 4 ⊢ (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 2825	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ↔ 𝑧 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
154	153	anbi2d 630	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑧 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))))
155	154	rexbidv 3297	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑧 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))))
156		eqeq1 2825	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ↔ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))
157	156	anbi2d 630	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})))
158	157	rexbidv 3297	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})))
159	155, 158	orbi12d 915	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((∃𝑣 ∈ ((𝑀 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 3297	. . . . 5 ⊢ (𝑦 = 𝑧 → (∃𝑢 ∈ ((𝑀 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 2650	. . . 4 ⊢ (∃*𝑦∃𝑢 ∈ ((𝑀 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 236	. . 3 ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → ∃*𝑦∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})))
163	162	alrimiv 1928	. 2 ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → ∀𝑥∃*𝑦∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})))
164		funopab 6390	. 2 ⊢ (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 236	1 ⊢ (Fun ((𝑀 Sat 𝐸)‘𝑁) → Fun {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑_m ω) ∣ ∀𝑘 ∈ 𝑀 ({⟨𝑖, 𝑘⟩} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 ∀wal 1535 = wceq 1537 ∈ wcel 2114 ∃*wmo 2620 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 {crab 3142 Vcvv 3494 ∖ cdif 3933 ∪ cun 3934 ∩ cin 3935 {csn 4567 ⟨cop 4573 {copab 5128 ↾ cres 5557 Fun wfun 6349 ‘cfv 6355 (class class class)co 7156 ωcom 7580 1^st c1st 7687 2^nd c2nd 7688 1_oc1o 8095 2_oc2o 8096 ↑_m cmap 8406 ⊼_𝑔cgna 32581 ∀_𝑔cgol 32582 Sat csat 32583

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fv 6363 df-ov 7159 df-om 7581 df-1st 7689 df-2nd 7690 df-1o 8102 df-2o 8103 df-gona 32588 df-goal 32589

This theorem is referenced by: satffunlem1 32654

W3C validator