satf0 - Mathbox for Mario Carneiro

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

Theorem satf0 34827

Description: The satisfaction predicate as function over wff codes in the empty model with an empty binary relation. (Contributed by AV, 14-Sep-2023.)

**Assertion**
Ref	Expression
satf0	⊢ (∅ Sat ∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))}) ↾ suc ω)

Distinct variable group: 𝑓,𝑖,𝑗,𝑢,𝑣,𝑥,𝑦

Proof of Theorem satf0 Dummy variables 𝑎 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 5307	. . 3 ⊢ ∅ ∈ V
2		satf 34808	. . 3 ⊢ ((∅ ∈ V ∧ ∅ ∈ V) → (∅ Sat ∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})}) ↾ suc ω))
3	1, 1, 2	mp2an 689	. 2 ⊢ (∅ Sat ∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})}) ↾ suc ω)
4		peano1 7883	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ ω
5	4	ne0ii 4337	. . . . . . . . . . . . . . . . . 18 ⊢ ω ≠ ∅
6		map0b 8883	. . . . . . . . . . . . . . . . . 18 ⊢ (ω ≠ ∅ → (∅ ↑_m ω) = ∅)
7	5, 6	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∅ ↑_m ω) = ∅
8	7	difeq1i 4118	. . . . . . . . . . . . . . . 16 ⊢ ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) = (∅ ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))
9		0dif 4401	. . . . . . . . . . . . . . . 16 ⊢ (∅ ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) = ∅
10	8, 9	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) = ∅
11	10	eqeq2i 2744	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ↔ 𝑦 = ∅)
12	11	anbi2i 622	. . . . . . . . . . . . 13 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅))
13	12	rexbii 3093	. . . . . . . . . . . 12 ⊢ (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ ∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅))
14		r19.41v 3187	. . . . . . . . . . . 12 ⊢ (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ↔ (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅))
15	13, 14	bitri 275	. . . . . . . . . . 11 ⊢ (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅))
16	7	rabeqi 3444	. . . . . . . . . . . . . . . 16 ⊢ {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = {𝑎 ∈ ∅ ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}
17		rab0 4382	. . . . . . . . . . . . . . . 16 ⊢ {𝑎 ∈ ∅ ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = ∅
18	16, 17	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = ∅
19	18	eqeq2i 2744	. . . . . . . . . . . . . 14 ⊢ (𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ↔ 𝑦 = ∅)
20	19	anbi2i 622	. . . . . . . . . . . . 13 ⊢ ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅))
21	20	rexbii 3093	. . . . . . . . . . . 12 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅))
22		r19.41v 3187	. . . . . . . . . . . 12 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅) ↔ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅))
23	21, 22	bitri 275	. . . . . . . . . . 11 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅))
24	15, 23	orbi12i 912	. . . . . . . . . 10 ⊢ ((∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ∨ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅)))
25	24	rexbii 3093	. . . . . . . . 9 ⊢ (∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ ∃𝑢 ∈ 𝑓 ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ∨ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅)))
26		andir 1006	. . . . . . . . . . 11 ⊢ (((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∧ 𝑦 = ∅) ↔ ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ∨ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅)))
27	26	bicomi 223	. . . . . . . . . 10 ⊢ (((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ∨ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅)) ↔ ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∧ 𝑦 = ∅))
28	27	rexbii 3093	. . . . . . . . 9 ⊢ (∃𝑢 ∈ 𝑓 ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ∨ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅)) ↔ ∃𝑢 ∈ 𝑓 ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∧ 𝑦 = ∅))
29		r19.41v 3187	. . . . . . . . 9 ⊢ (∃𝑢 ∈ 𝑓 ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∧ 𝑦 = ∅) ↔ (∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∧ 𝑦 = ∅))
30	25, 28, 29	3bitri 297	. . . . . . . 8 ⊢ (∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ (∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∧ 𝑦 = ∅))
31	30	biancomi 462	. . . . . . 7 ⊢ (∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
32	31	opabbii 5215	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))} = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}
33	32	uneq2i 4160	. . . . 5 ⊢ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))}) = (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})
34	33	mpteq2i 5253	. . . 4 ⊢ (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))
35	7	rabeqi 3444	. . . . . . . . . . 11 ⊢ {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)} = {𝑎 ∈ ∅ ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}
36		rab0 4382	. . . . . . . . . . 11 ⊢ {𝑎 ∈ ∅ ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)} = ∅
37	35, 36	eqtri 2759	. . . . . . . . . 10 ⊢ {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)} = ∅
38	37	eqeq2i 2744	. . . . . . . . 9 ⊢ (𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)} ↔ 𝑦 = ∅)
39	38	anbi2i 622	. . . . . . . 8 ⊢ ((𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}) ↔ (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅))
40	39	2rexbii 3128	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅))
41		r19.41vv 3223	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅))
42	40, 41	bitri 275	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅))
43	42	biancomi 462	. . . . 5 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}) ↔ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗)))
44	43	opabbii 5215	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})} = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))}
45		rdgeq12 8419	. . . 4 ⊢ (((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})) ∧ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})} = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))}) → rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})}) = rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))}))
46	34, 44, 45	mp2an 689	. . 3 ⊢ rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})}) = rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})
47	46	reseq1i 5977	. 2 ⊢ (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})}) ↾ suc ω) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))}) ↾ suc ω)
48	3, 47	eqtri 2759	1 ⊢ (∅ Sat ∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))}) ↾ suc ω)

Colors of variables: wff setvar class

Syntax hints: ∧ wa 395 ∨ wo 844 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 {crab 3431 Vcvv 3473 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ∅c0 4322 {csn 4628 ⟨cop 4634 class class class wbr 5148 {copab 5210 ↦ cmpt 5231 ↾ cres 5678 suc csuc 6366 ‘cfv 6543 (class class class)co 7412 ωcom 7859 1^st c1st 7977 2^nd c2nd 7978 reccrdg 8415 ↑_m cmap 8826 ∈_𝑔cgoe 34788 ⊼_𝑔cgna 34789 ∀_𝑔cgol 34790 Sat csat 34791

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-inf2 9642

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 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-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-1st 7979 df-2nd 7980 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-map 8828 df-sat 34798

This theorem is referenced by: satf0sucom 34828

W3C validator