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 35598

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 8402	. . . 4 ⊢ 1_o = suc ∅
2	1	fveq2i 6837	. . 3 ⊢ (𝑆‘1_o) = (𝑆‘suc ∅)
3	2	a1i 11	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = (𝑆‘suc ∅))
4		peano1 7836	. . 3 ⊢ ∅ ∈ ω
5		satfv1.s	. . . 4 ⊢ 𝑆 = (𝑀 Sat 𝐸)
6	5	satfvsuc 35596	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}))
7	4, 6	mp3an3 1458	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}))
8	5	satfv0 35593	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})
9	8	rexeqdv 3299	. . . . . 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 2740	. . . . . . 7 ⊢ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}
11		vex 3436	. . . . . . . . . . . . 13 ⊢ 𝑒 ∈ V
12		vex 3436	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
13	11, 12	op1std 7948	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (1^st ‘𝑜) = 𝑒)
14	13	oveq1d 7378	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔(1^st ‘𝑝)))
15	14	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝))))
16	11, 12	op2ndd 7949	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (2^nd ‘𝑜) = 𝑏)
17	16	ineq1d 4155	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)) = (𝑏 ∩ (2^nd ‘𝑝)))
18	17	difeq2d 4064	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))
19	18	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))))
20	15, 19	anbi12d 638	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
21	20	rexbidv 3164	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
22		eqidd 2741	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → 𝑛 = 𝑛)
23	22, 13	goaleq12d 35586	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ∀_𝑔𝑛(1^st ‘𝑜) = ∀_𝑔𝑛𝑒)
24	23	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ↔ 𝑥 = ∀_𝑔𝑛𝑒))
25	16	eleq2d 2826	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
26	25	ralbidv 3163	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
27	26	rabbidv 3399	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})
28	27	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))
29	24, 28	anbi12d 638	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
30	29	rexbidv 3164	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
31	21, 30	orbi12d 924	. . . . . . 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 5477	. . . . . 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 288	. . . . 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 35593	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})})
35	34	rexeqdv 3299	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
36		eqid 2740	. . . . . . . . . . 11 ⊢ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})}
37		vex 3436	. . . . . . . . . . . . . . 15 ⊢ 𝑐 ∈ V
38		vex 3436	. . . . . . . . . . . . . . 15 ⊢ 𝑑 ∈ V
39	37, 38	op1std 7948	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (1^st ‘𝑝) = 𝑐)
40	39	oveq2d 7379	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑒⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔𝑐))
41	40	eqeq2d 2751	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔𝑐)))
42	37, 38	op2ndd 7949	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (2^nd ‘𝑝) = 𝑑)
43	42	ineq2d 4156	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑏 ∩ (2^nd ‘𝑝)) = (𝑏 ∩ 𝑑))
44	43	difeq2d 4064	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))
45	44	eqeq2d 2751	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))
46	41, 45	anbi12d 638	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
47	36, 46	rexopabb 5477	. . . . . . . . . 10 ⊢ (∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
48	35, 47	bitrdi 288	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))))
49	48	orbi1d 922	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
50	49	anbi2d 636	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
51	50	2exbidv 1931	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
52		r19.41vv 3210	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
53		oveq1 7370	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐))
54	53	eqeq2d 2751	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = (𝑒⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐)))
55		ineq1 4149	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))
56	55	difeq2d 4064	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))
57	56	eqeq2d 2751	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))
58	54, 57	bi2anan9 644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
59	58	anbi2d 636	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
60	59	2exbidv 1931	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
61		eqidd 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑛 = 𝑛)
62		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑒 = (𝑖∈_𝑔𝑗))
63	61, 62	goaleq12d 35586	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → ∀_𝑔𝑛𝑒 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗))
64	63	eqeq2d 2751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = ∀_𝑔𝑛𝑒 ↔ 𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗)))
65		nfrab1 3412	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎{𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
66	65	nfeq2 2919	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
67		eleq2 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
68	67	ralbidv 3163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
69	66, 68	rabbid 3419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
70	69	eqeq2d 2751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
71	64, 70	bi2anan9 644	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
72	71	rexbidv 3164	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
73	60, 72	orbi12d 924	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
74	73	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
75		r19.41vv 3210	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
76		oveq2 7371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
77	76	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
78	77	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
79		ineq2 4150	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
80	79	difeq2d 4064	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
81		inrab 4251	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
82	81	difeq2i 4061	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
83		notrab 4257	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
84		ianor 989	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)))
85	84	rabbii 3397	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
86	82, 83, 85	3eqtri 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
87	80, 86	eqtrdi 2791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
88	87	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
89	88	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
90	78, 89	anbi12d 638	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})))
91	90	biimpa 477	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
92	91	reximi 3078	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
93	92	reximi 3078	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
94	75, 93	sylbir 236	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
95	94	exlimivv 1939	. . . . . . . . . . . . . . 15 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})))
97		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
98		simpll 772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
99		simplr 774	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω)
100		fveq1 6833	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑖) = (𝑏‘𝑖))
101		fveq1 6833	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑗) = (𝑏‘𝑗))
102	100, 101	breq12d 5092	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑏‘𝑖)𝐸(𝑏‘𝑗)))
103	102	cbvrabv 3402	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}
104	103	eleq2i 2832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
105	104	ralbii 3086	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
106	105	rabbii 3397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}}
107		satfv1lem 35597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
108	106, 107	eqtrid 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
109	97, 98, 99, 108	syl3anc 1379	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
110	109	eqeq2d 2751	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))
111	110	biimpd 230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} → 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))
112	111	anim2d 618	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
113	112	reximdva 3153	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
114	113	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
115	96, 114	orim12d 972	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
116	74, 115	sylbid 241	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
117	116	expimpd 454	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
118	117	reximdva 3153	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
119	118	reximia 3075	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
120	52, 119	sylbir 236	. . . . . . . 8 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
121	120	exlimivv 1939	. . . . . . 7 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
122		ovex 7396	. . . . . . . . . . . . 13 ⊢ (𝑖∈_𝑔𝑗) ∈ V
123		ovex 7396	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↑_m ω) ∈ V
124	123	rabex 5274	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V
125	122, 124	pm3.2i 471	. . . . . . . . . . . 12 ⊢ ((𝑖∈_𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V)
126		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)
127		eqid 2740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}
128	126, 127	pm3.2i 471	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})
129	86	eqcomi 2749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
130	129	eqeq2i 2753	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
131	130	biimpi 217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} → 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
132	131	anim2i 623	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))
133		ovex 7396	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) ∈ V
134	123	rabex 5274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ∈ V
135		eqeq1 2744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑐 = (𝑘∈_𝑔𝑙) ↔ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)))
136		eqeq1 2744	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
137	135, 136	bi2anan9 644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ↔ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
138	76	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
139	80	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))
140	138, 139	bi2anan9 644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))))
141	137, 140	anbi12d 638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))))
142	133, 134, 141	spc2ev 3552	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
143	128, 132, 142	sylancr 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
144	143	reximi 3078	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
145	144	reximi 3078	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
146	75	bicomi 225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
147	146	2exbii 1856	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
148		2ex2rexrot 3275	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
149	147, 148	bitri 276	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
150	145, 149	sylibr 235	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
151	150	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
152	109	eqcomd 2746	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
153	152	eqeq2d 2751	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
154	153	biimpd 230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} → 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
155	154	anim2d 618	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
156	155	reximdva 3153	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
157	151, 156	orim12d 972	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
158	157	imp 407	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
159		eqid 2740	. . . . . . . . . . . . . 14 ⊢ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)
160		eqid 2740	. . . . . . . . . . . . . 14 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
161	159, 160	pm3.2i 471	. . . . . . . . . . . . 13 ⊢ ((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
162	158, 161	jctil 524	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
163		eqeq1 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒 = (𝑖∈_𝑔𝑗) ↔ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)))
164		eqeq1 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
165	163, 164	bi2anan9 644	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
166	165, 73	anbi12d 638	. . . . . . . . . . . . 13 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))))
167	166	spc2egv 3544	. . . . . . . . . . . 12 ⊢ (((𝑖∈_𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V) → ((((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
168	125, 162, 167	mpsyl 68	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
169	168	ex 413	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
170	169	reximdva 3153	. . . . . . . . 9 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
171	170	reximia 3075	. . . . . . . 8 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
172	52	bicomi 225	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
173	172	2exbii 1856	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
174		2ex2rexrot 3275	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
175	173, 174	bitri 276	. . . . . . . 8 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
176	171, 175	sylibr 235	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
177	121, 176	impbii 210	. . . . . 6 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
178	51, 177	bitrdi 288	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
179	33, 178	bitrd 280	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
180	179	opabbidv 5145	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})
181	180	uneq2d 4105	. 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 2779	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 if-wif 1068 ∧ w3a 1092 = wceq 1547 ∃wex 1786 ∈ wcel 2119 ∀wral 3054 ∃wrex 3064 {crab 3392 Vcvv 3432 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ∅c0 4268 {csn 4562 ⟨cop 4568 class class class wbr 5079 {copab 5141 ↾ cres 5627 suc csuc 6319 ‘cfv 6492 (class class class)co 7363 ωcom 7813 1^st c1st 7936 2^nd c2nd 7937 1_oc1o 8395 ↑_m cmap 8770 ∈_𝑔cgoe 35568 ⊼_𝑔cgna 35569 ∀_𝑔cgol 35570 Sat csat 35571

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-inf2 9560

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-ifp 1069 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7366 df-oprab 7367 df-mpo 7368 df-om 7814 df-1st 7938 df-2nd 7939 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-map 8772 df-goel 35575 df-goal 35577 df-sat 35578

This theorem is referenced by: satfv1fvfmla1 35658

W3C validator