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 34352

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 34333	. . 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 691	. 2 ⊢ (∅ Sat ∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}))})), {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})}) ↾ suc ω)
4		peano1 7876	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ ω
5	4	ne0ii 4337	. . . . . . . . . . . . . . . . . 18 ⊢ ω ≠ ∅
6		map0b 8874	. . . . . . . . . . . . . . . . . 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 2761	. . . . . . . . . . . . . . 15 ⊢ ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) = ∅
11	10	eqeq2i 2746	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣))) ↔ 𝑦 = ∅)
12	11	anbi2i 624	. . . . . . . . . . . . 13 ⊢ ((𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅))
13	12	rexbii 3095	. . . . . . . . . . . 12 ⊢ (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ↔ ∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅))
14		r19.41v 3189	. . . . . . . . . . . 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 3446	. . . . . . . . . . . . . . . 16 ⊢ {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = {𝑎 ∈ ∅ ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}
17		rab0 4382	. . . . . . . . . . . . . . . 16 ⊢ {𝑎 ∈ ∅ ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = ∅
18	16, 17	eqtri 2761	. . . . . . . . . . . . . . 15 ⊢ {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} = ∅
19	18	eqeq2i 2746	. . . . . . . . . . . . . 14 ⊢ (𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)} ↔ 𝑦 = ∅)
20	19	anbi2i 624	. . . . . . . . . . . . 13 ⊢ ((𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅))
21	20	rexbii 3095	. . . . . . . . . . . 12 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅))
22		r19.41v 3189	. . . . . . . . . . . 12 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅) ↔ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅))
23	21, 22	bitri 275	. . . . . . . . . . 11 ⊢ (∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)}) ↔ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅))
24	15, 23	orbi12i 914	. . . . . . . . . 10 ⊢ ((∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ∨ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅)))
25	24	rexbii 3095	. . . . . . . . 9 ⊢ (∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 (𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ((∅ ↑_m ω) ∖ ((2^nd ‘𝑢) ∩ (2^nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ ∀𝑧 ∈ ∅ ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2^nd ‘𝑢)})) ↔ ∃𝑢 ∈ 𝑓 ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ∨ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅)))
26		andir 1008	. . . . . . . . . . 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 3095	. . . . . . . . 9 ⊢ (∃𝑢 ∈ 𝑓 ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∧ 𝑦 = ∅) ∨ (∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢) ∧ 𝑦 = ∅)) ↔ ∃𝑢 ∈ 𝑓 ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ∧ 𝑦 = ∅))
29		r19.41v 3189	. . . . . . . . 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 464	. . . . . . 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 3446	. . . . . . . . . . 11 ⊢ {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)} = {𝑎 ∈ ∅ ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}
36		rab0 4382	. . . . . . . . . . 11 ⊢ {𝑎 ∈ ∅ ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)} = ∅
37	35, 36	eqtri 2761	. . . . . . . . . 10 ⊢ {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)} = ∅
38	37	eqeq2i 2746	. . . . . . . . 9 ⊢ (𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)} ↔ 𝑦 = ∅)
39	38	anbi2i 624	. . . . . . . 8 ⊢ ((𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}) ↔ (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅))
40	39	2rexbii 3130	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅))
41		r19.41vv 3225	. . . . . . 7 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅))
42	40, 41	bitri 275	. . . . . 6 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}) ↔ (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = ∅))
43	42	biancomi 464	. . . . 5 ⊢ (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)}) ↔ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗)))
44	43	opabbii 5215	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖∈_𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (∅ ↑_m ω) ∣ (𝑎‘𝑖)∅(𝑎‘𝑗)})} = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))}
45		rdgeq12 8410	. . . 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 691	. . 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 5976	. 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 2761	1 ⊢ (∅ Sat ∅) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))}) ↾ suc ω)

Colors of variables: wff setvar class

Syntax hints: ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 {crab 3433 Vcvv 3475 ∖ 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 6364 ‘cfv 6541 (class class class)co 7406 ωcom 7852 1^st c1st 7970 2^nd c2nd 7971 reccrdg 8406 ↑_m cmap 8817 ∈_𝑔cgoe 34313 ⊼_𝑔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-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 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 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-ov 7409 df-oprab 7410 df-mpo 7411 df-om 7853 df-1st 7972 df-2nd 7973 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-map 8819 df-sat 34323

This theorem is referenced by: satf0sucom 34353

W3C validator