satfvsuclem1 - Mathbox for Mario Carneiro

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

Theorem satfvsuclem1 35581

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

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

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

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

**Proof of Theorem satfvsuclem1**
Step	Hyp	Ref	Expression
1		ancom 460	. . 3 ⊢ ((∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) ↔ (𝑦 ∈ 𝒫 (𝑀 ↑_m ω) ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))))
2	1	opabbii 5167	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))} = {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ 𝒫 (𝑀 ↑_m ω) ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})))}
3		ovex 7403	. . . . 5 ⊢ (𝑀 ↑_m ω) ∈ V
4	3	pwex 5329	. . . 4 ⊢ 𝒫 (𝑀 ↑_m ω) ∈ V
5	4	a1i 11	. . 3 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → 𝒫 (𝑀 ↑_m ω) ∈ V)
6		fvex 6857	. . . 4 ⊢ (𝑆‘𝑁) ∈ V
7		unab 4262	. . . . . . 7 ⊢ ({𝑥 ∣ ∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((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 ‘𝑢)}))}
8	6	abrexex 7918	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))} ∈ V
9		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
10	9	reximi 3076	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) → ∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)))
11	10	ss2abi 4020	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))} ⊆ {𝑥 ∣ ∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))}
12	8, 11	ssexi 5271	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))} ∈ V
13		omex 9566	. . . . . . . . . 10 ⊢ ω ∈ V
14	13	abrexex 7918	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)} ∈ V
15		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))
16	15	reximi 3076	. . . . . . . . . 10 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) → ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))
17	16	ss2abi 4020	. . . . . . . . 9 ⊢ {𝑥 ∣ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})} ⊆ {𝑥 ∣ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)}
18	14, 17	ssexi 5271	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})} ∈ V
19	12, 18	unex 7701	. . . . . . 7 ⊢ ({𝑥 ∣ ∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))))} ∪ {𝑥 ∣ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})}) ∈ V
20	7, 19	eqeltrri 2834	. . . . . 6 ⊢ {𝑥 ∣ (∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} ∈ V
21	20	a1i 11	. . . . 5 ⊢ ((((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → {𝑥 ∣ (∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} ∈ V)
22	21	ralrimiva 3130	. . . 4 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) → ∀𝑢 ∈ (𝑆‘𝑁){𝑥 ∣ (∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} ∈ V)
23		abrexex2g 7920	. . . 4 ⊢ (((𝑆‘𝑁) ∈ V ∧ ∀𝑢 ∈ (𝑆‘𝑁){𝑥 ∣ (∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} ∈ V) → {𝑥 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} ∈ V)
24	6, 22, 23	sylancr 588	. . 3 ⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω)) → {𝑥 ∣ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} ∈ V)
25	5, 24	opabex3rd 7922	. 2 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ 𝒫 (𝑀 ↑_m ω) ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})))} ∈ V)
26	2, 25	eqeltrid 2841	1 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)(𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((𝑀 ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑_m ω) ∣ ∀𝑧 ∈ 𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ∧ 𝑦 ∈ 𝒫 (𝑀 ↑_m ω))} ∈ V)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 {cab 2715 ∀wral 3052 ∃wrex 3062 {crab 3401 Vcvv 3442 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 𝒫 cpw 4556 {csn 4582 ⟨cop 4588 {copab 5162 ↾ cres 5636 ‘cfv 6502 (class class class)co 7370 ωcom 7820 1^st c1st 7943 2^nd c2nd 7944 ↑_m cmap 8777 ⊼_𝑔cgna 35556 ∀_𝑔cgol 35557 Sat csat 35558

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-inf2 9564

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-tr 5208 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fv 6510 df-ov 7373 df-om 7821

This theorem is referenced by: satfvsuclem2 35582

W3C validator