satfv1 - Mathbox for Mario Carneiro

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

Theorem satfv1 36097

Description: The value of the satisfaction predicate as function over wff codes of height 1. (Contributed by AV, 9-Nov-2023.)

**Hypothesis**
Ref	Expression
satfv1.s	⊢ 𝑆 = (𝑀 Sat 𝐸)

**Assertion**
Ref	Expression
satfv1	⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))

Distinct variable groups: 𝐸,𝑎,𝑖,𝑗,𝑘,𝑙,𝑥,𝑦 𝑛,𝐸,𝑧,𝑎,𝑖,𝑗,𝑥,𝑦 𝑀,𝑎,𝑖,𝑗,𝑘,𝑙,𝑥,𝑦 𝑛,𝑀,𝑧 𝑥,𝑆,𝑦 𝑥,𝑉,𝑦 𝑥,𝑊,𝑦 Allowed substitution hints: 𝑆(𝑧, 𝑖, 𝑗, 𝑘, 𝑛, 𝑎, 𝑙) 𝑉(𝑧, 𝑖, 𝑗, 𝑘, 𝑛, 𝑎, 𝑙) 𝑊(𝑧, 𝑖, 𝑗, 𝑘, 𝑛, 𝑎, 𝑙)

Proof of Theorem satfv1 Dummy variables 𝑏 𝑐 𝑑 𝑒 𝑜 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-1o 8460	. . . 4 ⊢ 1_o = suc ∅
2	1	fveq2i 6880	. . 3 ⊢ (𝑆‘1_o) = (𝑆‘suc ∅)
3	2	a1i 11	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = (𝑆‘suc ∅))
4		peano1 7889	. . 3 ⊢ ∅ ∈ ω
5		satfv1.s	. . . 4 ⊢ 𝑆 = (𝑀 Sat 𝐸)
6	5	satfvsuc 36095	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}))
7	4, 6	mp3an3 1479	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}))
8	5	satfv0 36092	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})
9	8	rexeqdv 3321	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑜 ∈ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))))
10		eqid 2761	. . . . . . 7 ⊢ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}
11		vex 3455	. . . . . . . . . . . . 13 ⊢ 𝑒 ∈ V
12		vex 3455	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
13	11, 12	op1std 8000	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (1^st ‘𝑜) = 𝑒)
14	13	oveq1d 7427	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔(1^st ‘𝑝)))
15	14	eqeq2d 2772	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝))))
16	11, 12	op2ndd 8001	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (2^nd ‘𝑜) = 𝑏)
17	16	ineq1d 4165	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)) = (𝑏 ∩ (2^nd ‘𝑝)))
18	17	difeq2d 4074	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))
19	18	eqeq2d 2772	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))))
20	15, 19	anbi12d 644	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
21	20	rexbidv 3187	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
22		eqidd 2762	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → 𝑛 = 𝑛)
23	22, 13	goaleq12d 36085	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ∀_𝑔𝑛(1^st ‘𝑜) = ∀_𝑔𝑛𝑒)
24	23	eqeq2d 2772	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ↔ 𝑥 = ∀_𝑔𝑛𝑒))
25	16	eleq2d 2847	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
26	25	ralbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
27	26	rabbidv 3420	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})
28	27	eqeq2d 2772	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))
29	24, 28	anbi12d 644	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
30	29	rexbidv 3187	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
31	21, 30	orbi12d 932	. . . . . . 7 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
32	10, 31	rexopabb 5502	. . . . . 6 ⊢ (∃𝑜 ∈ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
33	9, 32	bitrdi 290	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
34	5	satfv0 36092	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})})
35	34	rexeqdv 3321	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
36		eqid 2761	. . . . . . . . . . 11 ⊢ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})}
37		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑐 ∈ V
38		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑑 ∈ V
39	37, 38	op1std 8000	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (1^st ‘𝑝) = 𝑐)
40	39	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑒⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔𝑐))
41	40	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔𝑐)))
42	37, 38	op2ndd 8001	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (2^nd ‘𝑝) = 𝑑)
43	42	ineq2d 4166	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑏 ∩ (2^nd ‘𝑝)) = (𝑏 ∩ 𝑑))
44	43	difeq2d 4074	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))
45	44	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))
46	41, 45	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
47	36, 46	rexopabb 5502	. . . . . . . . . 10 ⊢ (∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
48	35, 47	bitrdi 290	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))))
49	48	orbi1d 930	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
50	49	anbi2d 642	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
51	50	2exbidv 1957	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
52		r19.41vv 3233	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
53		oveq1 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐))
54	53	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = (𝑒⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐)))
55		ineq1 4159	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))
56	55	difeq2d 4074	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))
57	56	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))
58	54, 57	bi2anan9 650	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
59	58	anbi2d 642	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
60	59	2exbidv 1957	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
61		eqidd 2762	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑛 = 𝑛)
62		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑒 = (𝑖∈_𝑔𝑗))
63	61, 62	goaleq12d 36085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → ∀_𝑔𝑛𝑒 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗))
64	63	eqeq2d 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = ∀_𝑔𝑛𝑒 ↔ 𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗)))
65		nfrab1 3432	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎{𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
66	65	nfeq2 2940	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
67		eleq2 2850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
68	67	ralbidv 3186	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
69	66, 68	rabbid 3439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
70	69	eqeq2d 2772	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
71	64, 70	bi2anan9 650	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
72	71	rexbidv 3187	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
73	60, 72	orbi12d 932	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
74	73	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
75		r19.41vv 3233	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
76		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
77	76	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
78	77	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
79		ineq2 4160	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
80	79	difeq2d 4074	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
81		inrab 4262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
82	81	difeq2i 4071	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
83		notrab 4268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
84		ianor 997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)))
85	84	rabbii 3418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
86	82, 83, 85	3eqtri 2788	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
87	80, 86	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
88	87	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
89	88	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
90	78, 89	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})))
91	90	biimpa 482	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
92	91	reximi 3101	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
93	92	reximi 3101	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
94	75, 93	sylbir 238	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
95	94	exlimivv 1965	. . . . . . . . . . . . . . 15 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})))
97		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
98		simpll 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
99		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω)
100		fveq1 6876	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑖) = (𝑏‘𝑖))
101		fveq1 6876	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑗) = (𝑏‘𝑗))
102	100, 101	breq12d 5116	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑏‘𝑖)𝐸(𝑏‘𝑗)))
103	102	cbvrabv 3423	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}
104	103	eleq2i 2853	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
105	104	ralbii 3109	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
106	105	rabbii 3418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}}
107		satfv1lem 36096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
108	106, 107	eqtrid 2808	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
109	97, 98, 99, 108	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
110	109	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))
111	110	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} → 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))
112	111	anim2d 624	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
113	112	reximdva 3176	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
114	113	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
115	96, 114	orim12d 979	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
116	74, 115	sylbid 243	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
117	116	expimpd 459	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
118	117	reximdva 3176	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
119	118	reximia 3098	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
120	52, 119	sylbir 238	. . . . . . . 8 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
121	120	exlimivv 1965	. . . . . . 7 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
122		ovex 7445	. . . . . . . . . . . . 13 ⊢ (𝑖∈_𝑔𝑗) ∈ V
123		ovex 7445	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↑_m ω) ∈ V
124	123	rabex 5300	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V
125	122, 124	pm3.2i 476	. . . . . . . . . . . 12 ⊢ ((𝑖∈_𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V)
126		eqid 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)
127		eqid 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}
128	126, 127	pm3.2i 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})
129	86	eqcomi 2770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
130	129	eqeq2i 2774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
131	130	biimpi 219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} → 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
132	131	anim2i 629	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))
133		ovex 7445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) ∈ V
134	123	rabex 5300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ∈ V
135		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑐 = (𝑘∈_𝑔𝑙) ↔ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)))
136		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
137	135, 136	bi2anan9 650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ↔ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
138	76	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
139	80	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))
140	138, 139	bi2anan9 650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))))
141	137, 140	anbi12d 644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))))
142	133, 134, 141	spc2ev 3562	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
143	128, 132, 142	sylancr 599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
144	143	reximi 3101	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
145	144	reximi 3101	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
146	75	bicomi 227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
147	146	2exbii 1882	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
148		2ex2rexrot 3298	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
149	147, 148	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
150	145, 149	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
151	150	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
152	109	eqcomd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
153	152	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
154	153	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} → 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
155	154	anim2d 624	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
156	155	reximdva 3176	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
157	151, 156	orim12d 979	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
158	157	imp 412	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
159		eqid 2761	. . . . . . . . . . . . . 14 ⊢ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)
160		eqid 2761	. . . . . . . . . . . . . 14 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
161	159, 160	pm3.2i 476	. . . . . . . . . . . . 13 ⊢ ((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
162	158, 161	jctil 529	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
163		eqeq1 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒 = (𝑖∈_𝑔𝑗) ↔ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)))
164		eqeq1 2765	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
165	163, 164	bi2anan9 650	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
166	165, 73	anbi12d 644	. . . . . . . . . . . . 13 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))))
167	166	spc2egv 3554	. . . . . . . . . . . 12 ⊢ (((𝑖∈_𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V) → ((((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
168	125, 162, 167	mpsyl 69	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
169	168	ex 418	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
170	169	reximdva 3176	. . . . . . . . 9 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
171	170	reximia 3098	. . . . . . . 8 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
172	52	bicomi 227	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
173	172	2exbii 1882	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
174		2ex2rexrot 3298	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
175	173, 174	bitri 278	. . . . . . . 8 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
176	171, 175	sylibr 237	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
177	121, 176	impbii 212	. . . . . 6 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
178	51, 177	bitrdi 290	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
179	33, 178	bitrd 282	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
180	179	opabbidv 5171	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})
181	180	uneq2d 4115	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))
182	3, 7, 181	3eqtrd 2800	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 if-wif 1078 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ∀wral 3077 ∃wrex 3087 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ∅c0 4279 {csn 4584 ⟨cop 4590 class class class wbr 5103 {copab 5167 ↾ cres 5653 suc csuc 6357 ‘cfv 6531 (class class class)co 7412 ωcom 7866 1^st c1st 7988 2^nd c2nd 7989 1_oc1o 8453 ↑_m cmap 8831 ∈_𝑔cgoe 36067 ⊼_𝑔cgna 36068 ∀_𝑔cgol 36069 Sat csat 36070

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-ifp 1079 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-map 8833 df-goel 36074 df-goal 36076 df-sat 36077

This theorem is used by: satfv1fvfmla1 36157

W3C validator