df-goal - Mathbox for Mario Carneiro

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

Definition df-goal 34985

Description: Define the Godel-set of universal quantification. Here 𝑁 ∈ ω corresponds to v_N , and 𝑈 represents another formula, and this expression is [∀𝑥𝜑] = ∀_𝑔𝑁𝑈 where 𝑥 is the 𝑁-th variable, 𝑈 = [𝜑] is the code for 𝜑. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

**Assertion**
Ref	Expression
df-goal	⊢ ∀_𝑔𝑁𝑈 = ⟨2_o, ⟨𝑁, 𝑈⟩⟩

**Detailed syntax breakdown of Definition df-goal**
Step	Hyp	Ref	Expression
1		cU	. . 3 class 𝑈
2		cN	. . 3 class 𝑁
3	1, 2	cgol 34978	. 2 class ∀_𝑔𝑁𝑈
4		c2o 8487	. . 3 class 2_o
5	2, 1	cop 4638	. . 3 class ⟨𝑁, 𝑈⟩
6	4, 5	cop 4638	. 2 class ⟨2_o, ⟨𝑁, 𝑈⟩⟩
7	3, 6	wceq 1533	1 wff ∀_𝑔𝑁𝑈 = ⟨2_o, ⟨𝑁, 𝑈⟩⟩

Colors of variables: wff setvar class

This definition is referenced by: goaleq12d 34994 gonanegoal 34995 sat1el2xp 35022 fmlaomn0 35033 goaln0 35036 goalrlem 35039 goalr 35040 fmla0disjsuc 35041 fmlasucdisj 35042 satffunlem1lem1 35045 satffunlem2lem1 35047

W3C validator

	
		OSZAR »