satf0suc - Mathbox for Mario Carneiro

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

Theorem satf0suc 35443

Description: The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation at a successor. (Contributed by AV, 19-Sep-2023.)

**Hypothesis**
Ref	Expression
satf0suc.s	⊢ 𝑆 = (∅ Sat ∅)

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

Distinct variable groups: 𝑢,𝑖,𝑣,𝑥,𝑦 𝑢,𝑁,𝑣,𝑥,𝑦 𝑢,𝑆,𝑣,𝑥,𝑦 Allowed substitution hints: 𝑆(𝑖) 𝑁(𝑖)

Proof of Theorem satf0suc Dummy variables 𝑓 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		satf0suc.s	. . . 4 ⊢ 𝑆 = (∅ Sat ∅)
2	1	fveq1i 6831	. . 3 ⊢ (𝑆‘suc 𝑁) = ((∅ Sat ∅)‘suc 𝑁)
3	2	a1i 11	. 2 ⊢ (𝑁 ∈ ω → (𝑆‘suc 𝑁) = ((∅ Sat ∅)‘suc 𝑁))
4		omsucelsucb 8385	. . 3 ⊢ (𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω)
5		satf0sucom 35440	. . 3 ⊢ (suc 𝑁 ∈ suc ω → ((∅ Sat ∅)‘suc 𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘suc 𝑁))
6	4, 5	sylbi 217	. 2 ⊢ (𝑁 ∈ ω → ((∅ Sat ∅)‘suc 𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘suc 𝑁))
7		nnon 7810	. . . 4 ⊢ (𝑁 ∈ ω → 𝑁 ∈ On)
8		rdgsuc 8351	. . . 4 ⊢ (𝑁 ∈ On → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘suc 𝑁) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘𝑁)))
9	7, 8	syl 17	. . 3 ⊢ (𝑁 ∈ ω → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘suc 𝑁) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘𝑁)))
10		elelsuc 6388	. . . . . 6 ⊢ (𝑁 ∈ ω → 𝑁 ∈ suc ω)
11		satf0sucom 35440	. . . . . 6 ⊢ (𝑁 ∈ suc ω → ((∅ Sat ∅)‘𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘𝑁))
12	10, 11	syl 17	. . . . 5 ⊢ (𝑁 ∈ ω → ((∅ Sat ∅)‘𝑁) = (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘𝑁))
13	1	eqcomi 2742	. . . . . 6 ⊢ (∅ Sat ∅) = 𝑆
14	13	fveq1i 6831	. . . . 5 ⊢ ((∅ Sat ∅)‘𝑁) = (𝑆‘𝑁)
15	12, 14	eqtr3di 2783	. . . 4 ⊢ (𝑁 ∈ ω → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘𝑁) = (𝑆‘𝑁))
16	15	fveq2d 6834	. . 3 ⊢ (𝑁 ∈ ω → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))‘(rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘𝑁)) = ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))‘(𝑆‘𝑁)))
17		eqidd 2734	. . . 4 ⊢ (𝑁 ∈ ω → (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})) = (𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})))
18		id 22	. . . . . 6 ⊢ (𝑓 = (𝑆‘𝑁) → 𝑓 = (𝑆‘𝑁))
19		rexeq 3289	. . . . . . . . . 10 ⊢ (𝑓 = (𝑆‘𝑁) → (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ↔ ∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣))))
20	19	orbi1d 916	. . . . . . . . 9 ⊢ (𝑓 = (𝑆‘𝑁) → ((∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
21	20	rexeqbi1dv 3306	. . . . . . . 8 ⊢ (𝑓 = (𝑆‘𝑁) → (∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)) ↔ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))))
22	21	anbi2d 630	. . . . . . 7 ⊢ (𝑓 = (𝑆‘𝑁) → ((𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢))) ↔ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))))
23	22	opabbidv 5161	. . . . . 6 ⊢ (𝑓 = (𝑆‘𝑁) → {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))} = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})
24	18, 23	uneq12d 4118	. . . . 5 ⊢ (𝑓 = (𝑆‘𝑁) → (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}) = ((𝑆‘𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))
25	24	adantl 481	. . . 4 ⊢ ((𝑁 ∈ ω ∧ 𝑓 = (𝑆‘𝑁)) → (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}) = ((𝑆‘𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))
26		fvex 6843	. . . . 5 ⊢ (𝑆‘𝑁) ∈ V
27	26	a1i 11	. . . 4 ⊢ (𝑁 ∈ ω → (𝑆‘𝑁) ∈ V)
28		omex 9542	. . . . . . 7 ⊢ ω ∈ V
29		satf0suclem 35442	. . . . . . 7 ⊢ (((𝑆‘𝑁) ∈ V ∧ (𝑆‘𝑁) ∈ V ∧ ω ∈ V) → {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))} ∈ V)
30	26, 26, 28, 29	mp3an 1463	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))} ∈ V
31	26, 30	unex 7685	. . . . 5 ⊢ ((𝑆‘𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}) ∈ V
32	31	a1i 11	. . . 4 ⊢ (𝑁 ∈ ω → ((𝑆‘𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}) ∈ V)
33	17, 25, 27, 32	fvmptd 6944	. . 3 ⊢ (𝑁 ∈ ω → ((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))‘(𝑆‘𝑁)) = ((𝑆‘𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))
34	9, 16, 33	3eqtrd 2772	. 2 ⊢ (𝑁 ∈ ω → (rec((𝑓 ∈ V ↦ (𝑓 ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ 𝑓 (∃𝑣 ∈ 𝑓 𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))})), {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈_𝑔𝑗))})‘suc 𝑁) = ((𝑆‘𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))
35	3, 6, 34	3eqtrd 2772	1 ⊢ (𝑁 ∈ ω → (𝑆‘suc 𝑁) = ((𝑆‘𝑁) ∪ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑁)(∃𝑣 ∈ (𝑆‘𝑁)𝑥 = ((1^st ‘𝑢)⊼_𝑔(1^st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀_𝑔𝑖(1^st ‘𝑢)))}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 ∃wrex 3057 Vcvv 3437 ∪ cun 3896 ∅c0 4282 {copab 5157 ↦ cmpt 5176 Oncon0 6313 suc csuc 6315 ‘cfv 6488 (class class class)co 7354 ωcom 7804 1^st c1st 7927 reccrdg 8336 ∈_𝑔cgoe 35400 ⊼_𝑔cgna 35401 ∀_𝑔cgol 35402 Sat csat 35403

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 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-inf2 9540

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-ral 3049 df-rex 3058 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-ov 7357 df-oprab 7358 df-mpo 7359 df-om 7805 df-1st 7929 df-2nd 7930 df-frecs 8219 df-wrecs 8250 df-recs 8299 df-rdg 8337 df-map 8760 df-sat 35410

This theorem is referenced by: satf0op 35444 satf0n0 35445 fmlafvel 35452

W3C validator