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 33325

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 8297	. . . 4 ⊢ 1_o = suc ∅
2	1	fveq2i 6777	. . 3 ⊢ (𝑆‘1_o) = (𝑆‘suc ∅)
3	2	a1i 11	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = (𝑆‘suc ∅))
4		peano1 7735	. . 3 ⊢ ∅ ∈ ω
5		satfv1.s	. . . 4 ⊢ 𝑆 = (𝑀 Sat 𝐸)
6	5	satfvsuc 33323	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}))
7	4, 6	mp3an3 1449	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}))
8	5	satfv0 33320	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})
9	8	rexeqdv 3349	. . . . . 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 2738	. . . . . . 7 ⊢ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}
11		vex 3436	. . . . . . . . . . . . 13 ⊢ 𝑒 ∈ V
12		vex 3436	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
13	11, 12	op1std 7841	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (1^st ‘𝑜) = 𝑒)
14	13	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔(1^st ‘𝑝)))
15	14	eqeq2d 2749	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝))))
16	11, 12	op2ndd 7842	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (2^nd ‘𝑜) = 𝑏)
17	16	ineq1d 4145	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)) = (𝑏 ∩ (2^nd ‘𝑝)))
18	17	difeq2d 4057	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))
19	18	eqeq2d 2749	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))))
20	15, 19	anbi12d 631	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
21	20	rexbidv 3226	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
22		eqidd 2739	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → 𝑛 = 𝑛)
23	22, 13	goaleq12d 33313	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ∀_𝑔𝑛(1^st ‘𝑜) = ∀_𝑔𝑛𝑒)
24	23	eqeq2d 2749	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ↔ 𝑥 = ∀_𝑔𝑛𝑒))
25	16	eleq2d 2824	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
26	25	ralbidv 3112	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
27	26	rabbidv 3414	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})
28	27	eqeq2d 2749	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))
29	24, 28	anbi12d 631	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
30	29	rexbidv 3226	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
31	21, 30	orbi12d 916	. . . . . . 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 5441	. . . . . 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 287	. . . . 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 33320	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})})
35	34	rexeqdv 3349	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
36		eqid 2738	. . . . . . . . . . 11 ⊢ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})}
37		vex 3436	. . . . . . . . . . . . . . 15 ⊢ 𝑐 ∈ V
38		vex 3436	. . . . . . . . . . . . . . 15 ⊢ 𝑑 ∈ V
39	37, 38	op1std 7841	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (1^st ‘𝑝) = 𝑐)
40	39	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑒⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔𝑐))
41	40	eqeq2d 2749	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔𝑐)))
42	37, 38	op2ndd 7842	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (2^nd ‘𝑝) = 𝑑)
43	42	ineq2d 4146	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑏 ∩ (2^nd ‘𝑝)) = (𝑏 ∩ 𝑑))
44	43	difeq2d 4057	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))
45	44	eqeq2d 2749	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))
46	41, 45	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
47	36, 46	rexopabb 5441	. . . . . . . . . 10 ⊢ (∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
48	35, 47	bitrdi 287	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))))
49	48	orbi1d 914	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
50	49	anbi2d 629	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
51	50	2exbidv 1927	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
52		r19.41vv 3278	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
53		oveq1 7282	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐))
54	53	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = (𝑒⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐)))
55		ineq1 4139	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))
56	55	difeq2d 4057	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))
57	56	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))
58	54, 57	bi2anan9 636	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
59	58	anbi2d 629	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
60	59	2exbidv 1927	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
61		eqidd 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑛 = 𝑛)
62		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑒 = (𝑖∈_𝑔𝑗))
63	61, 62	goaleq12d 33313	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → ∀_𝑔𝑛𝑒 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗))
64	63	eqeq2d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = ∀_𝑔𝑛𝑒 ↔ 𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗)))
65		nfrab1 3317	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎{𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
66	65	nfeq2 2924	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
67		eleq2 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
68	67	ralbidv 3112	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
69	66, 68	rabbid 3410	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
70	69	eqeq2d 2749	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
71	64, 70	bi2anan9 636	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
72	71	rexbidv 3226	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
73	60, 72	orbi12d 916	. . . . . . . . . . . . . 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 3278	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
76		oveq2 7283	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
77	76	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
78	77	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
79		ineq2 4140	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
80	79	difeq2d 4057	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
81		inrab 4240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
82	81	difeq2i 4054	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
83		notrab 4245	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
84		ianor 979	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)))
85	84	rabbii 3408	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
86	82, 83, 85	3eqtri 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
87	80, 86	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
88	87	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
89	88	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
90	78, 89	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})))
91	90	biimpa 477	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
92	91	reximi 3178	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
93	92	reximi 3178	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
94	75, 93	sylbir 234	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
95	94	exlimivv 1935	. . . . . . . . . . . . . . 15 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})))
97		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
98		simpll 764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
99		simplr 766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω)
100		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑖) = (𝑏‘𝑖))
101		fveq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑗) = (𝑏‘𝑗))
102	100, 101	breq12d 5087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑏‘𝑖)𝐸(𝑏‘𝑗)))
103	102	cbvrabv 3426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}
104	103	eleq2i 2830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
105	104	ralbii 3092	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
106	105	rabbii 3408	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}}
107		satfv1lem 33324	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
108	106, 107	eqtrid 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
109	97, 98, 99, 108	syl3anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
110	109	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))
111	110	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} → 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))
112	111	anim2d 612	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
113	112	reximdva 3203	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
114	113	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
115	96, 114	orim12d 962	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
116	74, 115	sylbid 239	. . . . . . . . . . . 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 3203	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
119	118	reximia 3176	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
120	52, 119	sylbir 234	. . . . . . . 8 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
121	120	exlimivv 1935	. . . . . . 7 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
122		ovex 7308	. . . . . . . . . . . . 13 ⊢ (𝑖∈_𝑔𝑗) ∈ V
123		ovex 7308	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↑_m ω) ∈ V
124	123	rabex 5256	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V
125	122, 124	pm3.2i 471	. . . . . . . . . . . 12 ⊢ ((𝑖∈_𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V)
126		eqid 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)
127		eqid 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}
128	126, 127	pm3.2i 471	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})
129	86	eqcomi 2747	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
130	129	eqeq2i 2751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
131	130	biimpi 215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} → 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
132	131	anim2i 617	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))
133		ovex 7308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) ∈ V
134	123	rabex 5256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ∈ V
135		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑐 = (𝑘∈_𝑔𝑙) ↔ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)))
136		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
137	135, 136	bi2anan9 636	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ↔ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
138	76	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
139	80	eqeq2d 2749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))
140	138, 139	bi2anan9 636	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))))
141	137, 140	anbi12d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))))
142	133, 134, 141	spc2ev 3546	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
143	128, 132, 142	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
144	143	reximi 3178	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
145	144	reximi 3178	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
146	75	bicomi 223	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
147	146	2exbii 1851	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
148		2ex2rexrot 3235	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
149	147, 148	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
150	145, 149	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
151	150	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
152	109	eqcomd 2744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
153	152	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
154	153	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} → 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
155	154	anim2d 612	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
156	155	reximdva 3203	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
157	151, 156	orim12d 962	. . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . 14 ⊢ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)
160		eqid 2738	. . . . . . . . . . . . . 14 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
161	159, 160	pm3.2i 471	. . . . . . . . . . . . 13 ⊢ ((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
162	158, 161	jctil 520	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
163		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒 = (𝑖∈_𝑔𝑗) ↔ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)))
164		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
165	163, 164	bi2anan9 636	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
166	165, 73	anbi12d 631	. . . . . . . . . . . . 13 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))))
167	166	spc2egv 3538	. . . . . . . . . . . 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 3203	. . . . . . . . 9 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
171	170	reximia 3176	. . . . . . . 8 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
172	52	bicomi 223	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
173	172	2exbii 1851	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
174		2ex2rexrot 3235	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
175	173, 174	bitri 274	. . . . . . . 8 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
176	171, 175	sylibr 233	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
177	121, 176	impbii 208	. . . . . 6 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
178	51, 177	bitrdi 287	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
179	33, 178	bitrd 278	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
180	179	opabbidv 5140	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})
181	180	uneq2d 4097	. 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 2782	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 if-wif 1060 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2106 ∀wral 3064 ∃wrex 3065 {crab 3068 Vcvv 3432 ∖ cdif 3884 ∪ cun 3885 ∩ cin 3886 ∅c0 4256 {csn 4561 ⟨cop 4567 class class class wbr 5074 {copab 5136 ↾ cres 5591 suc csuc 6268 ‘cfv 6433 (class class class)co 7275 ωcom 7712 1^st c1st 7829 2^nd c2nd 7830 1_oc1o 8290 ↑_m cmap 8615 ∈_𝑔cgoe 33295 ⊼_𝑔cgna 33296 ∀_𝑔cgol 33297 Sat csat 33298

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-inf2 9399

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-ifp 1061 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-map 8617 df-goel 33302 df-goal 33304 df-sat 33305

This theorem is referenced by: satfv1fvfmla1 33385

W3C validator