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 35726

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 8441	. . . 4 ⊢ 1_o = suc ∅
2	1	fveq2i 6874	. . 3 ⊢ (𝑆‘1_o) = (𝑆‘suc ∅)
3	2	a1i 11	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = (𝑆‘suc ∅))
4		peano1 7873	. . 3 ⊢ ∅ ∈ ω
5		satfv1.s	. . . 4 ⊢ 𝑆 = (𝑀 Sat 𝐸)
6	5	satfvsuc 35724	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ ∅ ∈ ω) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}))
7	4, 6	mp3an3 1474	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘suc ∅) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))}))
8	5	satfv0 35721	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})})
9	8	rexeqdv 3324	. . . . . 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 2765	. . . . . . 7 ⊢ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} = {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})}
11		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑒 ∈ V
12		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ V
13	11, 12	op1std 7984	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (1^st ‘𝑜) = 𝑒)
14	13	oveq1d 7415	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔(1^st ‘𝑝)))
15	14	eqeq2d 2776	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝))))
16	11, 12	op2ndd 7985	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (2^nd ‘𝑜) = 𝑏)
17	16	ineq1d 4174	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)) = (𝑏 ∩ (2^nd ‘𝑝)))
18	17	difeq2d 4083	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))
19	18	eqeq2d 2776	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))))
20	15, 19	anbi12d 643	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
21	20	rexbidv 3189	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
22		eqidd 2766	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → 𝑛 = 𝑛)
23	22, 13	goaleq12d 35714	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ∀_𝑔𝑛(1^st ‘𝑜) = ∀_𝑔𝑛𝑒)
24	23	eqeq2d 2776	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ↔ 𝑥 = ∀_𝑔𝑛𝑒))
25	16	eleq2d 2851	. . . . . . . . . . . . 13 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
26	25	ralbidv 3188	. . . . . . . . . . . 12 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜) ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏))
27	26	rabbidv 3424	. . . . . . . . . . 11 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})
28	27	eqeq2d 2776	. . . . . . . . . 10 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))
29	24, 28	anbi12d 643	. . . . . . . . 9 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → ((𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
30	29	rexbidv 3189	. . . . . . . 8 ⊢ (𝑜 = ⟨𝑒, 𝑏⟩ → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))
31	21, 30	orbi12d 931	. . . . . . 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 5503	. . . . . 6 ⊢ (∃𝑜 ∈ {⟨𝑒, 𝑏⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})} (∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
33	9, 32	bitrdi 290	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
34	5	satfv0 35721	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘∅) = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})})
35	34	rexeqdv 3324	. . . . . . . . . 10 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))))))
36		eqid 2765	. . . . . . . . . . 11 ⊢ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} = {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})}
37		vex 3461	. . . . . . . . . . . . . . 15 ⊢ 𝑐 ∈ V
38		vex 3461	. . . . . . . . . . . . . . 15 ⊢ 𝑑 ∈ V
39	37, 38	op1std 7984	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (1^st ‘𝑝) = 𝑐)
40	39	oveq2d 7416	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑒⊼_𝑔(1^st ‘𝑝)) = (𝑒⊼_𝑔𝑐))
41	40	eqeq2d 2776	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ↔ 𝑥 = (𝑒⊼_𝑔𝑐)))
42	37, 38	op2ndd 7985	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (2^nd ‘𝑝) = 𝑑)
43	42	ineq2d 4175	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑏 ∩ (2^nd ‘𝑝)) = (𝑏 ∩ 𝑑))
44	43	difeq2d 4083	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))
45	44	eqeq2d 2776	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))
46	41, 45	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑝 = ⟨𝑐, 𝑑⟩ → ((𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
47	36, 46	rexopabb 5503	. . . . . . . . . 10 ⊢ (∃𝑝 ∈ {⟨𝑐, 𝑑⟩ ∣ ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})} (𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))))
48	35, 47	bitrdi 290	. . . . . . . . 9 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))))))
49	48	orbi1d 929	. . . . . . . 8 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
50	49	anbi2d 641	. . . . . . 7 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
51	50	2exbidv 1947	. . . . . 6 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
52		r19.41vv 3235	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
53		oveq1 7407	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐))
54	53	eqeq2d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = (𝑒⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐)))
55		ineq1 4168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))
56	55	difeq2d 4083	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))
57	56	eqeq2d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))
58	54, 57	bi2anan9 649	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
59	58	anbi2d 641	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
60	59	2exbidv 1947	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ↔ ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
61		eqidd 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑛 = 𝑛)
62		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → 𝑒 = (𝑖∈_𝑔𝑗))
63	61, 62	goaleq12d 35714	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → ∀_𝑔𝑛𝑒 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗))
64	63	eqeq2d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑥 = ∀_𝑔𝑛𝑒 ↔ 𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗)))
65		nfrab1 3437	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑎{𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
66	65	nfeq2 2944	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑎 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
67		eleq2 2854	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
68	67	ralbidv 3188	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏 ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
69	66, 68	rabbid 3444	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
70	69	eqeq2d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
71	64, 70	bi2anan9 649	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
72	71	rexbidv 3189	. . . . . . . . . . . . . . 15 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}) ↔ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
73	60, 72	orbi12d 931	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
74	73	adantl 486	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) ↔ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
75		r19.41vv 3235	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
76		oveq2 7408	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
77	76	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)))
78	77	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
79		ineq2 4169	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑) = ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
80	79	difeq2d 4083	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
81		inrab 4271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
82	81	difeq2i 4080	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
83		notrab 4277	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 ↑_m ω) ∖ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
84		ianor 997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙)) ↔ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙)))
85	84	rabbii 3422	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ¬ ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ∧ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
86	82, 83, 85	3eqtri 2792	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}
87	80, 86	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})
88	87	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
89	88	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
90	78, 89	anbi12d 643	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})))
91	90	biimpa 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
92	91	reximi 3103	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
93	92	reximi 3103	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
94	75, 93	sylbir 238	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
95	94	exlimivv 1955	. . . . . . . . . . . . . . 15 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}))
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))})))
97		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
98		simpll 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑖 ∈ ω)
99		simplr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → 𝑗 ∈ ω)
100		fveq1 6870	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑖) = (𝑏‘𝑖))
101		fveq1 6870	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑗) = (𝑏‘𝑗))
102	100, 101	breq12d 5118	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑖)𝐸(𝑎‘𝑗) ↔ (𝑏‘𝑖)𝐸(𝑏‘𝑗)))
103	102	cbvrabv 3427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}
104	103	eleq2i 2857	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
105	104	ralbii 3111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)})
106	105	rabbii 3422	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}}
107		satfv1lem 35725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑏 ∈ (𝑀 ↑_m ω) ∣ (𝑏‘𝑖)𝐸(𝑏‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
108	106, 107	eqtrid 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑛 ∈ ω ∧ 𝑖 ∈ ω ∧ 𝑗 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
109	97, 98, 99, 108	syl3anc 1394	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})
110	109	eqeq2d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))
111	110	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}} → 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))
112	111	anim2d 623	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
113	112	reximdva 3178	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
114	113	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
115	96, 114	orim12d 979	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
116	74, 115	sylbid 243	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})) → ((∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
117	116	expimpd 458	. . . . . . . . . . 11 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
118	117	reximdva 3178	. . . . . . . . . 10 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
119	118	reximia 3100	. . . . . . . . 9 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
120	52, 119	sylbir 238	. . . . . . . 8 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
121	120	exlimivv 1955	. . . . . . 7 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
122		ovex 7433	. . . . . . . . . . . . 13 ⊢ (𝑖∈_𝑔𝑗) ∈ V
123		ovex 7433	. . . . . . . . . . . . . 14 ⊢ (𝑀 ↑_m ω) ∈ V
124	123	rabex 5300	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V
125	122, 124	pm3.2i 475	. . . . . . . . . . . 12 ⊢ ((𝑖∈_𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V)
126		eqid 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)
127		eqid 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}
128	126, 127	pm3.2i 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})
129	86	eqcomi 2774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
130	129	eqeq2i 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
131	130	biimpi 219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))} → 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
132	131	anim2i 628	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))
133		ovex 7433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘∈_𝑔𝑙) ∈ V
134	123	rabex 5300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ∈ V
135		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑐 = (𝑘∈_𝑔𝑙) ↔ (𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙)))
136		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))
137	135, 136	bi2anan9 649	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ↔ ((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))
138	76	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑘∈_𝑔𝑙) → (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ↔ 𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙))))
139	80	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} → (𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))
140	138, 139	bi2anan9 649	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))) ↔ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))))
141	137, 140	anbi12d 643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) → (((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ (((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}))))))
142	133, 134, 141	spc2ev 3569	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑘∈_𝑔𝑙) = (𝑘∈_𝑔𝑙) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)})))) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
143	128, 132, 142	sylancr 598	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
144	143	reximi 3103	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
145	144	reximi 3103	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
146	75	bicomi 227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
147	146	2exbii 1872	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
148		2ex2rexrot 3300	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑐∃𝑑∃𝑘 ∈ ω ∃𝑙 ∈ ω ((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
149	147, 148	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ↔ ∃𝑘 ∈ ω ∃𝑙 ∈ ω ∃𝑐∃𝑑((𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
150	145, 149	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))))
151	150	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) → ∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑))))))
152	109	eqcomd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})
153	152	eqeq2d 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
154	153	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))} → 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))
155	154	anim2d 623	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑛 ∈ ω) → ((𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
156	155	reximdva 3178	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}) → ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
157	151, 156	orim12d 979	. . . . . . . . . . . . . 14 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
158	157	imp 411	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))
159		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)
160		eqid 2765	. . . . . . . . . . . . . 14 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}
161	159, 160	pm3.2i 475	. . . . . . . . . . . . 13 ⊢ ((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})
162	158, 161	jctil 528	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → (((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))))
163		eqeq1 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = (𝑖∈_𝑔𝑗) → (𝑒 = (𝑖∈_𝑔𝑗) ↔ (𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗)))
164		eqeq1 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} → (𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}))
165	163, 164	bi2anan9 649	. . . . . . . . . . . . . 14 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ↔ ((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)})))
166	165, 73	anbi12d 643	. . . . . . . . . . . . 13 ⊢ ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) → (((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ (((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}})))))
167	166	spc2egv 3561	. . . . . . . . . . . 12 ⊢ (((𝑖∈_𝑔𝑗) ∈ V ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∈ V) → ((((𝑖∈_𝑔𝑗) = (𝑖∈_𝑔𝑗) ∧ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ({𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)} ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}}))) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
168	125, 162, 167	mpsyl 69	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
169	168	ex 417	. . . . . . . . . 10 ⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ((∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
170	169	reximdva 3178	. . . . . . . . 9 ⊢ (𝑖 ∈ ω → (∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏})))))
171	170	reximia 3100	. . . . . . . 8 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
172	52	bicomi 227	. . . . . . . . . 10 ⊢ ((∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
173	172	2exbii 1872	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
174		2ex2rexrot 3300	. . . . . . . . 9 ⊢ (∃𝑒∃𝑏∃𝑖 ∈ ω ∃𝑗 ∈ ω ((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
175	173, 174	bitri 278	. . . . . . . 8 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω ∃𝑒∃𝑏((𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
176	171, 175	sylibr 237	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})) → ∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))))
177	121, 176	impbii 212	. . . . . 6 ⊢ (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑐∃𝑑(∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑐 = (𝑘∈_𝑔𝑙) ∧ 𝑑 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑘)𝐸(𝑎‘𝑙)}) ∧ (𝑥 = (𝑒⊼_𝑔𝑐) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ 𝑑)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))})))
178	51, 177	bitrdi 290	. . . . 5 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑒∃𝑏(∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑒 = (𝑖∈_𝑔𝑗) ∧ 𝑏 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (𝑎‘𝑖)𝐸(𝑎‘𝑗)}) ∧ (∃𝑝 ∈ (𝑆‘∅)(𝑥 = (𝑒⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ (𝑏 ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛𝑒 ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ 𝑏}))) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
179	33, 178	bitrd 282	. . . 4 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)})) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))))
180	179	opabbidv 5171	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑜 ∈ (𝑆‘∅)(∃𝑝 ∈ (𝑆‘∅)(𝑥 = ((1^st ‘𝑜)⊼_𝑔(1^st ‘𝑝)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑜) ∩ (2^nd ‘𝑝)))) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(1^st ‘𝑜) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑛, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑛}))) ∈ (2^nd ‘𝑜)}))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))})
181	180	uneq2d 4124	. 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 2804	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (𝑆‘1_o) = ((𝑆‘∅) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (∃𝑘 ∈ ω ∃𝑙 ∈ ω (𝑥 = ((𝑖∈_𝑔𝑗)⊼_𝑔(𝑘∈_𝑔𝑙)) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ (¬ (𝑎‘𝑖)𝐸(𝑎‘𝑗) ∨ ¬ (𝑎‘𝑘)𝐸(𝑎‘𝑙))}) ∨ ∃𝑛 ∈ ω (𝑥 = ∀_𝑔𝑛(𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 if-(𝑖 = 𝑛, if-(𝑗 = 𝑛, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝑗)), if-(𝑗 = 𝑛, (𝑎‘𝑖)𝐸𝑧, (𝑎‘𝑖)𝐸(𝑎‘𝑗)))}))}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 if-wif 1076 ∧ w3a 1101 = wceq 1563 ∃wex 1802 ∈ wcel 2145 ∀wral 3079 ∃wrex 3089 {crab 3417 Vcvv 3457 ∖ cdif 3904 ∪ cun 3905 ∩ cin 3906 ∅c0 4288 {csn 4585 ⟨cop 4591 class class class wbr 5105 {copab 5167 ↾ cres 5654 suc csuc 6352 ‘cfv 6525 (class class class)co 7400 ωcom 7850 1^st c1st 7972 2^nd c2nd 7973 1_oc1o 8434 ↑_m cmap 8812 ∈_𝑔cgoe 35696 ⊼_𝑔cgna 35697 ∀_𝑔cgol 35698 Sat csat 35699

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-inf2 9598

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-ifp 1077 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-1st 7974 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-map 8814 df-goel 35703 df-goal 35705 df-sat 35706

This theorem is referenced by: satfv1fvfmla1 35786

W3C validator