df-sat

Description: Define the satisfaction predicate. This recursive construction builds up a function over wff codes (see satff ) and simultaneously defines the set of assignments to all variables from M that makes the coded wff true in the model M , where e. is interpreted as the binary relation E on M .

The interpretation of the statement S e. ( ( ( M Sat E )n )U ) is that for the model <. M , E >. , S :om --> M is a valuation of the variables (v0 = ( S(/) ) , v_1 = ( S1o ) , etc.) and U is a code for a wff using e. , -/\ , A. that is true under the assignment S . The function is defined by finite recursion; ( ( M Sat E )n ) only operates on wffs of depth at most n e.om , and ( ( M Sat E )om ) = U_ n e. _om ( ( M Sat E )n ) operates on all wffs.

		Ref	Expression
	Assertion	df-sat	⊢ Sat = ( 𝑚 ∈ V , 𝑒 ∈ V ↦ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csat	⊢ Sat
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		ve	⊢ 𝑒
4		vf	⊢ 𝑓
5	4	cv	⊢ 𝑓
6		vx	⊢ 𝑥
7		vy	⊢ 𝑦
8		vu	⊢ 𝑢
9		vv	⊢ 𝑣
10	6	cv	⊢ 𝑥
11		c1st	⊢ 1^st
12	8	cv	⊢ 𝑢
13	12 11	cfv	⊢ ( 1^st ‘ 𝑢 )
14		cgna	⊢ ⊼_𝑔
15	9	cv	⊢ 𝑣
16	15 11	cfv	⊢ ( 1^st ‘ 𝑣 )
17	13 16 14	co	⊢ ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) )
18	10 17	wceq	⊢ 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) )
19	7	cv	⊢ 𝑦
20	1	cv	⊢ 𝑚
21		cmap	⊢ ↑_m
22		com	⊢ ω
23	20 22 21	co	⊢ ( 𝑚 ↑_m ω )
24		c2nd	⊢ 2^nd
25	12 24	cfv	⊢ ( 2^nd ‘ 𝑢 )
26	15 24	cfv	⊢ ( 2^nd ‘ 𝑣 )
27	25 26	cin	⊢ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) )
28	23 27	cdif	⊢ ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
29	19 28	wceq	⊢ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
30	18 29	wa	⊢ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
31	30 9 5	wrex	⊢ ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) )
32		vi	⊢ 𝑖
33	32	cv	⊢ 𝑖
34	13 33	cgol	⊢ ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 )
35	10 34	wceq	⊢ 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 )
36		va	⊢ 𝑎
37		vz	⊢ 𝑧
38	37	cv	⊢ 𝑧
39	33 38	cop	⊢ ⟨ 𝑖 , 𝑧 ⟩
40	39	csn	⊢ { ⟨ 𝑖 , 𝑧 ⟩ }
41	36	cv	⊢ 𝑎
42	33	csn	⊢ { 𝑖 }
43	22 42	cdif	⊢ ( ω ∖ { 𝑖 } )
44	41 43	cres	⊢ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) )
45	40 44	cun	⊢ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) )
46	45 25	wcel	⊢ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 )
47	46 37 20	wral	⊢ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 )
48	47 36 23	crab	⊢ { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) }
49	19 48	wceq	⊢ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) }
50	35 49	wa	⊢ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } )
51	50 32 22	wrex	⊢ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } )
52	31 51	wo	⊢ ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) )
53	52 8 5	wrex	⊢ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) )
54	53 6 7	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) }
55	5 54	cun	⊢ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } )
56	4 2 55	cmpt	⊢ ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
57		vj	⊢ 𝑗
58		cgoe	⊢ ∈_𝑔
59	57	cv	⊢ 𝑗
60	33 59 58	co	⊢ ( 𝑖 ∈_𝑔 𝑗 )
61	10 60	wceq	⊢ 𝑥 = ( 𝑖 ∈_𝑔 𝑗 )
62	33 41	cfv	⊢ ( 𝑎 ‘ 𝑖 )
63	3	cv	⊢ 𝑒
64	59 41	cfv	⊢ ( 𝑎 ‘ 𝑗 )
65	62 64 63	wbr	⊢ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 )
66	65 36 23	crab	⊢ { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) }
67	19 66	wceq	⊢ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) }
68	61 67	wa	⊢ ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } )
69	68 57 22	wrex	⊢ ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } )
70	69 32 22	wrex	⊢ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } )
71	70 6 7	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } ) }
72	56 71	crdg	⊢ rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } ) } )
73	22	csuc	⊢ suc ω
74	72 73	cres	⊢ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω )
75	1 3 2 2 74	cmpo	⊢ ( 𝑚 ∈ V , 𝑒 ∈ V ↦ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω ) )
76	0 75	wceq	⊢ Sat = ( 𝑚 ∈ V , 𝑒 ∈ V ↦ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑚 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ∀ 𝑧 ∈ 𝑚 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑚 ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝑒 ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω ) )

Metamath Proof Explorer

Definition df-sat

Detailed syntax breakdown