satffunlem2lem1 - Mathbox for Mario Carneiro

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

Theorem satffunlem2lem1 36148

Description: Lemma 1 for satffunlem2 36152. (Contributed by AV, 28-Oct-2023.)

**Hypotheses**
Ref	Expression
satffunlem2lem1.s	⊢ 𝑆 = (𝑀 Sat 𝐸)
satffunlem2lem1.a	⊢ 𝐴 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
satffunlem2lem1.b	⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}

**Assertion**
Ref	Expression
satffunlem2lem1	⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))})

Distinct variable groups: 𝑦,𝐴 𝑦,𝐵 𝑖,𝑀,𝑢 𝑣,𝑀,𝑢 𝑖,𝑁,𝑢,𝑥,𝑦 𝑣,𝑁,𝑥,𝑦 𝑆,𝑖,𝑢,𝑥,𝑦 𝑣,𝑆 𝑖,𝑎,𝑢 𝑣,𝑎 𝑧,𝑖,𝑢 𝑧,𝑣 Allowed substitution hints: 𝐴(𝑥, 𝑧, 𝑣, 𝑢, 𝑖, 𝑎) 𝐵(𝑥, 𝑧, 𝑣, 𝑢, 𝑖, 𝑎) 𝑆(𝑧, 𝑎) 𝐸(𝑥, 𝑦, 𝑧, 𝑣, 𝑢, 𝑖, 𝑎) 𝑀(𝑥, 𝑦, 𝑧, 𝑎) 𝑁(𝑧, 𝑎)

Proof of Theorem satffunlem2lem1 Dummy variables 𝑗 𝑠 𝑤 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → 𝑢 = 𝑠)
2	1	fveq2d 6887	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (1^st ‘𝑢) = (1^st ‘𝑠))
3		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → 𝑣 = 𝑟)
4	3	fveq2d 6887	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (1^st ‘𝑣) = (1^st ‘𝑟))
5	2, 4	oveq12d 7436	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)))
6	5	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ↔ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))))
7		satffunlem2lem1.a	. . . . . . . . . . . . . 14 ⊢ 𝐴 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
8	1	fveq2d 6887	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (2^nd ‘𝑢) = (2^nd ‘𝑠))
9	3	fveq2d 6887	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (2^nd ‘𝑣) = (2^nd ‘𝑟))
10	8, 9	ineq12d 4167	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)) = ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))
11	10	difeq2d 4074	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))
12	7, 11	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → 𝐴 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))
13	12	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑦 = 𝐴 ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))))
14	6, 13	anbi12d 644	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))))
15	14	cbvrexdva 3244	. . . . . . . . . 10 ⊢ (𝑢 = 𝑠 → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))))
16		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
17		fveq2 6883	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑠 → (1^st ‘𝑢) = (1^st ‘𝑠))
18	17	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (1^st ‘𝑢) = (1^st ‘𝑠))
19	16, 18	goaleq12d 36095	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑗(1^st ‘𝑠))
20	19	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ 𝑥 = ∀_𝑔𝑗(1^st ‘𝑠)))
21		satffunlem2lem1.b	. . . . . . . . . . . . . 14 ⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}
22	21	eqeq2i 2774	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐵 ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})
23		opeq1 4833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑗 → ⟨𝑖, 𝑧⟩ = ⟨𝑗, 𝑧⟩)
24	23	sneqd 4596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → {⟨𝑖, 𝑧⟩} = {⟨𝑗, 𝑧⟩})
25		sneq 4594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑗 → {𝑖} = {𝑗})
26	25	difeq2d 4074	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑗 → (ω ∖ {𝑖}) = (ω ∖ {𝑗}))
27	26	reseq2d 5970	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → (𝑎 ↾ (ω ∖ {𝑖})) = (𝑎 ↾ (ω ∖ {𝑗})))
28	24, 27	uneq12d 4116	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) = ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))))
29	28	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) = ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))))
30		fveq2 6883	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑠 → (2^nd ‘𝑢) = (2^nd ‘𝑠))
31	30	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (2^nd ‘𝑢) = (2^nd ‘𝑠))
32	29, 31	eleq12d 2855	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢) ↔ ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)))
33	32	ralbidv 3186	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢) ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)))
34	33	rabbidv 3420	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})
35	34	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}))
36	22, 35	bitrid 286	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑦 = 𝐵 ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}))
37	20, 36	anbi12d 644	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})))
38	37	cbvrexdva 3244	. . . . . . . . . 10 ⊢ (𝑢 = 𝑠 → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})))
39	15, 38	orbi12d 932	. . . . . . . . 9 ⊢ (𝑢 = 𝑠 → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}))))
40	39	cbvrexvw 3242	. . . . . . . 8 ⊢ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})))
41		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑟 → (1^st ‘𝑣) = (1^st ‘𝑟))
42	17, 41	oveqan12d 7437	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)))
43	42	eqeq2d 2772	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ↔ 𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟))))
44	7	eqeq2i 2774	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐴 ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))
45		fveq2 6883	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑟 → (2^nd ‘𝑣) = (2^nd ‘𝑟))
46	30, 45	ineqan12d 4168	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)) = ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))
47	46	difeq2d 4074	. . . . . . . . . . . . 13 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))
48	47	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))))
49	44, 48	bitrid 286	. . . . . . . . . . 11 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑦 = 𝐴 ↔ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))))
50	43, 49	anbi12d 644	. . . . . . . . . 10 ⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))))
51	50	cbvrexdva 3244	. . . . . . . . 9 ⊢ (𝑢 = 𝑠 → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))))
52	51	cbvrexvw 3242	. . . . . . . 8 ⊢ (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑠 ∈ (𝑆‘𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))))
53	40, 52	orbi12i 928	. . . . . . 7 ⊢ ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})) ∨ ∃𝑠 ∈ (𝑆‘𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))))
54		simp-5l 797	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → Fun (𝑆‘suc 𝑁))
55		eldifi 4078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑠 ∈ (𝑆‘suc 𝑁))
56	55	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁))
57	56	anim1i 627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
58	57	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
59		eldifi 4078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁))
60	59	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → 𝑢 ∈ (𝑆‘suc 𝑁))
61	60	anim1i 627	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
62	54, 58, 61	3jca 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
63		id 23	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))))
64	7	eqeq2i 2774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝐴 ↔ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))
65	64	biimpi 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝐴 → 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))
66	65	anim2i 629	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
67		satffunlem 36145	. . . . . . . . . . . . . . . . . . 19 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))) → 𝑦 = 𝑤)
68	62, 63, 66, 67	syl3an 1178	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
69	68	3exp 1137	. . . . . . . . . . . . . . . . 17 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
70	69	com23 87	. . . . . . . . . . . . . . . 16 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
71	70	rexlimdva 3164	. . . . . . . . . . . . . . 15 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
72		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ↔ ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ∀_𝑔𝑖(1^st ‘𝑢)))
73		fvex 6896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑠) ∈ V
74		fvex 6896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑟) ∈ V
75		gonafv 36094	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1^st ‘𝑠) ∈ V ∧ (1^st ‘𝑟) ∈ V) → ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩)
76	73, 74, 75	mp2an 705	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩
77		df-goal 36086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀_𝑔𝑖(1^st ‘𝑢) = ⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩
78	76, 77	eqeq12i 2779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ∀_𝑔𝑖(1^st ‘𝑢) ↔ ⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩ = ⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩)
79		1oex 8479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1_o ∈ V
80		opex 5432	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩ ∈ V
81	79, 80	opth 5445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩ = ⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ ↔ (1_o = 2_o ∧ ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩ = ⟨𝑖, (1^st ‘𝑢)⟩))
82		1one2o 8648	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1_o ≠ 2_o
83		df-ne 2957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (1_o ≠ 2_o ↔ ¬ 1_o = 2_o)
84		pm2.21 124	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (¬ 1_o = 2_o → (1_o = 2_o → 𝑦 = 𝑤))
85	83, 84	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1_o ≠ 2_o → (1_o = 2_o → 𝑦 = 𝑤))
86	82, 85	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1_o = 2_o → 𝑦 = 𝑤)
87	86	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1_o = 2_o ∧ ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩ = ⟨𝑖, (1^st ‘𝑢)⟩) → 𝑦 = 𝑤)
88	81, 87	sylbi 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨1_o, ⟨(1^st ‘𝑠), (1^st ‘𝑟)⟩⟩ = ⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ → 𝑦 = 𝑤)
89	78, 88	sylbi 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) = ∀_𝑔𝑖(1^st ‘𝑢) → 𝑦 = 𝑤)
90	72, 89	biimtrdi 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → 𝑦 = 𝑤))
91	90	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → 𝑦 = 𝑤))
92	91	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤))
93	92	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤))
94	93	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
95	94	rexlimdva 3164	. . . . . . . . . . . . . . 15 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
96	71, 95	jaod 873	. . . . . . . . . . . . . 14 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
97	96	rexlimdva 3164	. . . . . . . . . . . . 13 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
98		simp-4l 795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → Fun (𝑆‘suc 𝑁))
99	57	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
100		ssel 3925	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁) → (𝑢 ∈ (𝑆‘𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
101	100	ad3antlr 744	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
102	101	com12 33	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ (𝑆‘𝑁) → ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁)))
103	102	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁)))
104	103	impcom 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁))
105		eldifi 4078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑣 ∈ (𝑆‘suc 𝑁))
106	105	ad2antll 742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑣 ∈ (𝑆‘suc 𝑁))
107	104, 106	jca 521	. . . . . . . . . . . . . . . . . 18 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
108	98, 99, 107	3jca 1146	. . . . . . . . . . . . . . . . 17 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
109	108, 63, 66, 67	syl3an 1178	. . . . . . . . . . . . . . . 16 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
110	109	3exp 1137	. . . . . . . . . . . . . . 15 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
111	110	com23 87	. . . . . . . . . . . . . 14 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
112	111	rexlimdvva 3220	. . . . . . . . . . . . 13 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
113	97, 112	jaod 873	. . . . . . . . . . . 12 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → 𝑦 = 𝑤)))
114	113	com23 87	. . . . . . . . . . 11 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
115	114	rexlimdva 3164	. . . . . . . . . 10 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
116		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ↔ ∀_𝑔𝑗(1^st ‘𝑠) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
117		df-goal 36086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∀_𝑔𝑗(1^st ‘𝑠) = ⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩
118		fvex 6896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑢) ∈ V
119		fvex 6896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1^st ‘𝑣) ∈ V
120		gonafv 36094	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1^st ‘𝑢) ∈ V ∧ (1^st ‘𝑣) ∈ V) → ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩)
121	118, 119, 120	mp2an 705	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩
122	117, 121	eqeq12i 2779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀_𝑔𝑗(1^st ‘𝑠) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ↔ ⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩)
123		2oex 8481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2_o ∈ V
124		opex 5432	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ⟨𝑗, (1^st ‘𝑠)⟩ ∈ V
125	123, 124	opth 5445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ ↔ (2_o = 1_o ∧ ⟨𝑗, (1^st ‘𝑠)⟩ = ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩))
126	86	eqcoms 2769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2_o = 1_o → 𝑦 = 𝑤)
127	126	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2_o = 1_o ∧ ⟨𝑗, (1^st ‘𝑠)⟩ = ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩) → 𝑦 = 𝑤)
128	125, 127	sylbi 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩ = ⟨1_o, ⟨(1^st ‘𝑢), (1^st ‘𝑣)⟩⟩ → 𝑦 = 𝑤)
129	122, 128	sylbi 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀_𝑔𝑗(1^st ‘𝑠) = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → 𝑦 = 𝑤)
130	116, 129	biimtrdi 256	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → 𝑦 = 𝑤))
131	130	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → 𝑦 = 𝑤))
132	131	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤))
133	132	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤))
134	133	rexlimivw 3160	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤))
135	134	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
136		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ↔ ∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑗(1^st ‘𝑠)))
137	77, 117	eqeq12i 2779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑗(1^st ‘𝑠) ↔ ⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ = ⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩)
138		opex 5432	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ⟨𝑖, (1^st ‘𝑢)⟩ ∈ V
139	123, 138	opth 5445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨2_o, ⟨𝑖, (1^st ‘𝑢)⟩⟩ = ⟨2_o, ⟨𝑗, (1^st ‘𝑠)⟩⟩ ↔ (2_o = 2_o ∧ ⟨𝑖, (1^st ‘𝑢)⟩ = ⟨𝑗, (1^st ‘𝑠)⟩))
140		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑖 ∈ V
141	140, 118	opth 5445	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨𝑖, (1^st ‘𝑢)⟩ = ⟨𝑗, (1^st ‘𝑠)⟩ ↔ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)))
142	141	anbi2i 635	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((2_o = 2_o ∧ ⟨𝑖, (1^st ‘𝑢)⟩ = ⟨𝑗, (1^st ‘𝑠)⟩) ↔ (2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠))))
143	137, 139, 142	3bitri 300	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀_𝑔𝑖(1^st ‘𝑢) = ∀_𝑔𝑗(1^st ‘𝑠) ↔ (2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠))))
144	136, 143	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ↔ (2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)))))
145	144	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ↔ (2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)))))
146	55	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑠 ∈ (𝑆‘suc 𝑁)))
147		funfv1st2nd 8055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ 𝑠 ∈ (𝑆‘suc 𝑁)) → ((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠))
148	147	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Fun (𝑆‘suc 𝑁) → (𝑠 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠)))
149	148	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠)))
150		funfv1st2nd 8055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ((𝑆‘suc 𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢))
151	150	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Fun (𝑆‘suc 𝑁) → (𝑢 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢)))
152	151	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢)))
153		fveqeq2 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) ↔ ((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑢)))
154		eqtr2 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑢) ∧ ((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠)) → (2^nd ‘𝑢) = (2^nd ‘𝑠))
155	28	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑖 = 𝑗 → ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))))
156	155	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) = ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))))
157		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → (2^nd ‘𝑢) = (2^nd ‘𝑠))
158	157	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → (2^nd ‘𝑠) = (2^nd ‘𝑢))
159	156, 158	eleq12d 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → (({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠) ↔ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)))
160	159	ralbidv 3186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → (∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠) ↔ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)))
161	160	rabbidv 3420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})
162	161, 21	eqtr4di 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} = 𝐵)
163		eqeq12 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} ∧ 𝑤 = 𝐵) → (𝑦 = 𝑤 ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} = 𝐵))
164	162, 163	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((2^nd ‘𝑢) = (2^nd ‘𝑠) ∧ 𝑖 = 𝑗) → ((𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
165	164	exp4b 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((2^nd ‘𝑢) = (2^nd ‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))
166	154, 165	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑢) ∧ ((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠)) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))
167	166	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑢) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))
168	153, 167	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))))
169	168	com24 96	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((1^st ‘𝑢) = (1^st ‘𝑠) → (𝑖 = 𝑗 → (((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))))
170	169	impcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))
171	170	com13 89	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑆‘suc 𝑁)‘(1^st ‘𝑢)) = (2^nd ‘𝑢) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))
172	59, 152, 171	syl56 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))))
173	172	com23 87	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (((𝑆‘suc 𝑁)‘(1^st ‘𝑠)) = (2^nd ‘𝑠) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))))
174	146, 149, 173	3syld 61	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))))
175	174	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))
176	175	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))
177	176	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))
178	177	adantld 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠))) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))
179	178	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ((2_o = 2_o ∧ (𝑖 = 𝑗 ∧ (1^st ‘𝑢) = (1^st ‘𝑠))) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))
180	145, 179	sylbid 243	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) → (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))
181	180	impd 416	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → (𝑤 = 𝐵 → 𝑦 = 𝑤)))
182	181	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → (𝑤 = 𝐵 → 𝑦 = 𝑤))))
183	182	com34 92	. . . . . . . . . . . . . . . . 17 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) → (𝑤 = 𝐵 → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤))))
184	183	impd 416	. . . . . . . . . . . . . . . 16 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
185	184	rexlimdva 3164	. . . . . . . . . . . . . . 15 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
186	135, 185	jaod 873	. . . . . . . . . . . . . 14 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
187	186	rexlimdva 3164	. . . . . . . . . . . . 13 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
188	133	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
189	188	rexlimdva 3164	. . . . . . . . . . . . . 14 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
190	189	rexlimdva 3164	. . . . . . . . . . . . 13 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
191	187, 190	jaod 873	. . . . . . . . . . . 12 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → 𝑦 = 𝑤)))
192	191	com23 87	. . . . . . . . . . 11 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → ((𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
193	192	rexlimdva 3164	. . . . . . . . . 10 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)}) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
194	115, 193	jaod 873	. . . . . . . . 9 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
195	194	rexlimdva 3164	. . . . . . . 8 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
196		simplll 787	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → Fun (𝑆‘suc 𝑁))
197		ssel 3925	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁) → (𝑠 ∈ (𝑆‘𝑁) → 𝑠 ∈ (𝑆‘suc 𝑁)))
198	197	adantrd 497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁) → ((𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁)))
199	198	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ((𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁)))
200	199	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑠 ∈ (𝑆‘suc 𝑁))
201		eldifi 4078	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑟 ∈ (𝑆‘suc 𝑁))
202	201	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑟 ∈ (𝑆‘suc 𝑁))
203	200, 202	jca 521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
204	203	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
205	59	anim1i 627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
206	205	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
207	196, 204, 206	3jca 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
208	207	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
209		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴))) → (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))))
210	66	ad2antll 742	. . . . . . . . . . . . . . . . . 18 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴))) → (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))))
211	208, 209, 210, 67	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤)
212	211	exp32 426	. . . . . . . . . . . . . . . 16 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
213	212	impancom 457	. . . . . . . . . . . . . . 15 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) → ((𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
214	213	expdimp 458	. . . . . . . . . . . . . 14 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (𝑣 ∈ (𝑆‘suc 𝑁) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
215	214	rexlimdv 3162	. . . . . . . . . . . . 13 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))
216	90	adantrd 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
217	216	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
218	217	ad3antlr 744	. . . . . . . . . . . . . 14 ⊢ ((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
219	218	rexlimdva 3164	. . . . . . . . . . . . 13 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤))
220	215, 219	jaod 873	. . . . . . . . . . . 12 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) → 𝑦 = 𝑤))
221	220	rexlimdva 3164	. . . . . . . . . . 11 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) → 𝑦 = 𝑤))
222		simplll 787	. . . . . . . . . . . . . . . 16 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → Fun (𝑆‘suc 𝑁))
223	203	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)))
224	100	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
225	224	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑢 ∈ (𝑆‘𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁)))
226	225	com12 33	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝑆‘𝑁) → (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁)))
227	226	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁)))
228	227	impcom 413	. . . . . . . . . . . . . . . . 17 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁))
229	105	ad2antll 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑣 ∈ (𝑆‘suc 𝑁))
230	228, 229	jca 521	. . . . . . . . . . . . . . . 16 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))
231	222, 223, 230	3jca 1146	. . . . . . . . . . . . . . 15 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))))
232	231, 63, 66, 67	syl3an 1178	. . . . . . . . . . . . . 14 ⊢ (((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∧ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)
233	232	3exp 1137	. . . . . . . . . . . . 13 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
234	233	impancom 457	. . . . . . . . . . . 12 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) → ((𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)))
235	234	rexlimdvv 3219	. . . . . . . . . . 11 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))
236	221, 235	jaod 873	. . . . . . . . . 10 ⊢ ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))
237	236	ex 418	. . . . . . . . 9 ⊢ (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → ((𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
238	237	rexlimdvva 3220	. . . . . . . 8 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (∃𝑠 ∈ (𝑆‘𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
239	195, 238	jaod 873	. . . . . . 7 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ((∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀_𝑔𝑗(1^st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑗, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2^nd ‘𝑠)})) ∨ ∃𝑠 ∈ (𝑆‘𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑠)⊼_𝑔(1^st ‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑠) ∩ (2^nd ‘𝑟))))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
240	53, 239	biimtrid 245	. . . . . 6 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)))
241	240	impd 416	. . . . 5 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤))
242	241	alrimivv 1961	. . . 4 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ∀𝑦∀𝑤(((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤))
243		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 = 𝐴 ↔ 𝑤 = 𝐴))
244	243	anbi2d 642	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)))
245	244	rexbidv 3187	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)))
246		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → (𝑦 = 𝐵 ↔ 𝑤 = 𝐵))
247	246	anbi2d 642	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)))
248	247	rexbidv 3187	. . . . . . . 8 ⊢ (𝑦 = 𝑤 → (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)))
249	245, 248	orbi12d 932	. . . . . . 7 ⊢ (𝑦 = 𝑤 → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵))))
250	249	rexbidv 3187	. . . . . 6 ⊢ (𝑦 = 𝑤 → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵))))
251	244	2rexbidv 3228	. . . . . 6 ⊢ (𝑦 = 𝑤 → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴)))
252	250, 251	orbi12d 932	. . . . 5 ⊢ (𝑦 = 𝑤 → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴))))
253	252	mo4 2592	. . . 4 ⊢ (∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)) ↔ ∀𝑦∀𝑤(((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤))
254	242, 253	sylibr 237	. . 3 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)))
255	254	alrimiv 1960	. 2 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ∀𝑥∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)))
256		funopab 6573	. 2 ⊢ (Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))} ↔ ∀𝑥∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴)))
257	255, 256	sylibr 237	1 ⊢ ((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → Fun {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = 𝐴))})

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∈ wcel 2145 ∃*wmo 2563 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 {csn 4584 ⟨cop 4590 {copab 5167 ↾ cres 5653 suc csuc 6363 Fun wfun 6531 ‘cfv 6537 (class class class)co 7418 ωcom 7875 1^st c1st 7997 2^nd c2nd 7998 1_oc1o 8462 2_oc2o 8463 ↑_m cmap 8840 ⊼_𝑔cgna 36078 ∀_𝑔cgol 36079 Sat csat 36080

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

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fv 6545 df-ov 7421 df-om 7876 df-1st 7999 df-2nd 8000 df-1o 8469 df-2o 8470 df-gona 36085 df-goal 36086

This theorem is used by: satffunlem2 36152

W3C validator