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 36214

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 8479	. . . 4 ⊢ 1_o = suc ∅
2	1	fveq2i 6888	. . 3 ⊢ (𝑆‘1_o) = (𝑆‘suc ∅)
3	2	a1i 11	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = (𝑆‘suc ∅))
4		peano1 7900	. . 3 ⊢ ∅ ∈ ω
5		satfv1.s	. . . 4 ⊢ 𝑆 = (𝑀 Sat 𝐸)
6	5	satfvsuc 36212	. . 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 36209	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})
9	8	rexeqdv 3320	. . . . . 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 2760	. . . . . . 7 ⊢ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}
11		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑒 ∈ V
12		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
13	11, 12	op1std 8011	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (1^st ‘𝑜) = 𝑒)
14	13	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔(1^st ‘𝑝)))
15	14	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝))))
16	11, 12	op2ndd 8012	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (2^nd ‘𝑜) = 𝑏)
17	16	ineq1d 4116	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)) = (𝑏 ∩ (2^nd ‘𝑝)))
18	17	difeq2d 4063	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))
19	18	eqeq2d 2771	. . . . . . . . . 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 3186	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
22		eqidd 2761	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → 𝑛 = 𝑛)
23	22, 13	goaleq12d 36202	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ∀_𝑔𝑛(1^st ‘𝑜) = ∀_𝑔𝑛𝑒)
24	23	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ↔ 𝑥 = ∀_𝑔𝑛𝑒))
25	16	eleq2d 2846	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
26	25	ralbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
27	26	rabbidv 3419	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})
28	27	eqeq2d 2771	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))
29	24, 28	anbi12d 644	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
30	29	rexbidv 3186	. . . . . . . 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 5501	. . . . . 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 36209	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})})
35	34	rexeqdv 3320	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
36		eqid 2760	. . . . . . . . . . 11 ⊢ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})}
37		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑐 ∈ V
38		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑑 ∈ V
39	37, 38	op1std 8011	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (1^st ‘𝑝) = 𝑐)
40	39	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑒⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔𝑐))
41	40	eqeq2d 2771	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔𝑐)))
42	37, 38	op2ndd 8012	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (2^nd ‘𝑝) = 𝑑)
43	42	ineq2d 4117	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑏 ∩ (2^nd ‘𝑝)) = (𝑏 ∩ 𝑑))
44	43	difeq2d 4063	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))
45	44	eqeq2d 2771	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))
46	41, 45	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
47	36, 46	rexopabb 5501	. . . . . . . . . 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 1956	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
52		r19.41vv 3232	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
53		oveq1 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐))
54	53	eqeq2d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = (𝑒⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐)))
55		ineq1 4110	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))
56	55	difeq2d 4063	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))
57	56	eqeq2d 2771	. . . . . . . . . . . . . . . . . 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 1956	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
61		eqidd 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑛 = 𝑛)
62		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑒 = (𝑖∈_𝑔𝑗))
63	61, 62	goaleq12d 36202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → ∀_𝑔𝑛𝑒 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗))
64	63	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = ∀_𝑔𝑛𝑒 ↔ 𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗)))
65		nfrab1 3431	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎{𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
66	65	nfeq2 2939	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
67		eleq2 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
68	67	ralbidv 3185	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
69	66, 68	rabbid 3438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
70	69	eqeq2d 2771	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
71	64, 70	bi2anan9 650	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
72	71	rexbidv 3186	. . . . . . . . . . . . . . 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 3232	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
76		oveq2 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
77	76	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
78	77	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
79		ineq2 4111	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
80	79	difeq2d 4063	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
81		inrab 4261	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
82	81	difeq2i 4060	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
83		notrab 4267	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
84		ianor 997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)))
85	84	rabbii 3417	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
86	82, 83, 85	3eqtri 2787	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
87	80, 86	eqtrdi 2811	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
88	87	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . 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 3100	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
93	92	reximi 3100	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
94	75, 93	sylbir 238	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
95	94	exlimivv 1964	. . . . . . . . . . . . . . 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 6884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑖) = (𝑏‘𝑖))
101		fveq1 6884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑗) = (𝑏‘𝑗))
102	100, 101	breq12d 5115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑏‘𝑖)𝐸(𝑏‘𝑗)))
103	102	cbvrabv 3422	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}
104	103	eleq2i 2852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
105	104	ralbii 3108	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
106	105	rabbii 3417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}}
107		satfv1lem 36213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
108	106, 107	eqtrid 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
109	97, 98, 99, 108	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
110	109	eqeq2d 2771	. . . . . . . . . . . . . . . . . 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 3175	. . . . . . . . . . . . . . 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 3175	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
119	118	reximia 3097	. . . . . . . . 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 1964	. . . . . . 7 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
122		ovex 7453	. . . . . . . . . . . . 13 ⊢ (𝑖∈_𝑔𝑗) ∈ V
123		ovex 7453	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↑_m ω) ∈ V
124	123	rabex 5299	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V
125	122, 124	pm3.2i 476	. . . . . . . . . . . 12 ⊢ ((𝑖∈_𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V)
126		eqid 2760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)
127		eqid 2760	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}
128	126, 127	pm3.2i 476	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})
129	86	eqcomi 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
130	129	eqeq2i 2773	. . . . . . . . . . . . . . . . . . . . . 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 7453	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) ∈ V
134	123	rabex 5299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ∈ V
135		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑐 = (𝑘∈_𝑔𝑙) ↔ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)))
136		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
137	135, 136	bi2anan9 650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ↔ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
138	76	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
139	80	eqeq2d 2771	. . . . . . . . . . . . . . . . . . . . . . 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 3561	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
143	128, 132, 142	sylancr 599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
144	143	reximi 3100	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
145	144	reximi 3100	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
146	75	bicomi 227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
147	146	2exbii 1881	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
148		2ex2rexrot 3297	. . . . . . . . . . . . . . . . . 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 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
153	152	eqeq2d 2771	. . . . . . . . . . . . . . . . . 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 3175	. . . . . . . . . . . . . . 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 2760	. . . . . . . . . . . . . 14 ⊢ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)
160		eqid 2760	. . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒 = (𝑖∈_𝑔𝑗) ↔ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)))
164		eqeq1 2764	. . . . . . . . . . . . . . 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 3553	. . . . . . . . . . . 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 3175	. . . . . . . . 9 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
171	170	reximia 3097	. . . . . . . 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 1881	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
174		2ex2rexrot 3297	. . . . . . . . 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 5170	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})
181	180	uneq2d 4167	. 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 2799	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 1569 ∃wex 1811 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ∖ cdif 4045 ∩ cin 4089 ∪ cun 4149 ∅c0 4278 {csn 4584 ⟨cop 4834 class class class wbr 5102 {copab 5166 ↾ cres 5652 suc csuc 6364 ‘cfv 6538 (class class class)co 7420 ωcom 7877 1^st c1st 7999 2^nd c2nd 8000 1_oc1o 8472 ↑_m cmap 8850 ∈_𝑔cgoe 36184 ⊼_𝑔cgna 36185 ∀_𝑔cgol 36186 Sat csat 36187

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9645

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 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-map 8852 df-goel 36191 df-goal 36193 df-sat 36194

This theorem is used by: satfv1fvfmla1 36274

W3C validator