satfvsuclem2 - Mathbox for Mario Carneiro

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

Theorem satfvsuclem2 34340

Description: Lemma 2 for satfvsuc 34341. (Contributed by AV, 8-Oct-2023.)

**Hypothesis**
Ref	Expression
satfv0.s	⊢ 𝑆 = (𝑀 Sat 𝐸)

**Assertion**
Ref	Expression
satfvsuclem2	⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} ∈ V)

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

**Proof of Theorem satfvsuclem2**
Step	Hyp	Ref	Expression
1		r19.41v 3189	. . . . . . 7 ⊢ (∃𝑣 ∈ (𝑆‘𝑁)((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) ↔ (∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
2		r19.41v 3189	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) ↔ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
3	1, 2	orbi12i 914	. . . . . 6 ⊢ ((∃𝑣 ∈ (𝑆‘𝑁)((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) ∨ ∃𝑖 ∈ ω ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))) ↔ ((∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) ∨ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))))
4		ovex 7439	. . . . . . . . . . . 12 ⊢ (𝑀 ↑_m ω) ∈ V
5		difelpw 5351	. . . . . . . . . . . 12 ⊢ ((𝑀 ↑_m ω) ∈ V → ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑_m ω))
6	4, 5	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑_m ω)
7		eleq1 2822	. . . . . . . . . . 11 ⊢ (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → (𝑦 ∈ 𝒫 (𝑀 ↑_m ω) ↔ ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∈ 𝒫 (𝑀 ↑_m ω)))
8	6, 7	mpbiri 258	. . . . . . . . . 10 ⊢ (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) → 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))
9	8	pm4.71i 561	. . . . . . . . 9 ⊢ (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ↔ (𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
10	9	bianass 641	. . . . . . . 8 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
11	10	rexbii 3095	. . . . . . 7 ⊢ (∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ ∃𝑣 ∈ (𝑆‘𝑁)((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
12		rabelpw 5352	. . . . . . . . . . . 12 ⊢ ((𝑀 ↑_m ω) ∈ V → {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑_m ω))
13	4, 12	ax-mp 5	. . . . . . . . . . 11 ⊢ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑_m ω)
14		eleq1 2822	. . . . . . . . . . 11 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → (𝑦 ∈ 𝒫 (𝑀 ↑_m ω) ↔ {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∈ 𝒫 (𝑀 ↑_m ω)))
15	13, 14	mpbiri 258	. . . . . . . . . 10 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} → 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))
16	15	pm4.71i 561	. . . . . . . . 9 ⊢ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ↔ (𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
17	16	bianass 641	. . . . . . . 8 ⊢ ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
18	17	rexbii 3095	. . . . . . 7 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
19	11, 18	orbi12i 914	. . . . . 6 ⊢ ((∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ (∃𝑣 ∈ (𝑆‘𝑁)((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) ∨ ∃𝑖 ∈ ω ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))))
20		andir 1008	. . . . . 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 ‘𝑣)))) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) ∨ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))))
21	3, 19, 20	3bitr4i 303	. . . . 5 ⊢ ((∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ ((∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
22	21	rexbii 3095	. . . 4 ⊢ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ ∃𝑢 ∈ (𝑆‘𝑁)((∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
23		r19.41v 3189	. . . 4 ⊢ (∃𝑢 ∈ (𝑆‘𝑁)((∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((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 ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
24	22, 23	bitri 275	. . 3 ⊢ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)))
25	24	opabbii 5215	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} = {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))}
26		satfv0.s	. . 3 ⊢ 𝑆 = (𝑀 Sat 𝐸)
27	26	satfvsuclem1 34339	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))} ∈ V)
28	25, 27	eqeltrid 2838	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} ∈ V)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 {crab 3433 Vcvv 3475 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 𝒫 cpw 4602 {csn 4628 ⟨cop 4634 {copab 5210 ↾ cres 5678 ‘cfv 6541 (class class class)co 7406 ωcom 7852 1^st c1st 7970 2^nd c2nd 7971 ↑_m cmap 8817 ⊼_𝑔cgna 34314 ∀_𝑔cgol 34315 Sat csat 34316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-tr 5266 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fv 6549 df-ov 7409 df-om 7853

This theorem is referenced by: satfvsuc 34341

W3C validator