satefvfmla0

Description: The simplified satisfaction predicate for wff codes of height 0. (Contributed by AV, 4-Nov-2023)

		Ref	Expression
	Assertion	satefvfmla0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( 𝑀 Sat_∈ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		satefv	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( 𝑀 Sat_∈ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑋 ) )
2		incom	⊢ ( E ∩ ( 𝑀 × 𝑀 ) ) = ( ( 𝑀 × 𝑀 ) ∩ E )
3		sqxpexg	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 × 𝑀 ) ∈ V )
4		inex1g	⊢ ( ( 𝑀 × 𝑀 ) ∈ V → ( ( 𝑀 × 𝑀 ) ∩ E ) ∈ V )
5	3 4	syl	⊢ ( 𝑀 ∈ 𝑉 → ( ( 𝑀 × 𝑀 ) ∩ E ) ∈ V )
6	2 5	eqeltrid	⊢ ( 𝑀 ∈ 𝑉 → ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V )
7	6	ancli	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) )
8	7	adantr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) )
9		satom	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) → ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) = ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) )
10	8 9	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) = ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) )
11	10	fveq1d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑋 ) = ( ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ‘ 𝑋 ) )
12		satfun	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) → ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀 ↑_m ω ) )
13	8 12	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀 ↑_m ω ) )
14	13	ffund	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → Fun ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) )
15	10	eqcomd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) = ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) )
16	15	funeqd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( Fun ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ↔ Fun ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ) )
17	14 16	mpbird	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → Fun ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) )
18		peano1	⊢ ∅ ∈ ω
19	18	a1i	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ∅ ∈ ω )
20	18	a1i	⊢ ( 𝑀 ∈ 𝑉 → ∅ ∈ ω )
21		satfdmfmla	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ∧ ∅ ∈ ω ) → dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) = ( Fmla ‘ ∅ ) )
22	6 20 21	mpd3an23	⊢ ( 𝑀 ∈ 𝑉 → dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) = ( Fmla ‘ ∅ ) )
23	22	eqcomd	⊢ ( 𝑀 ∈ 𝑉 → ( Fmla ‘ ∅ ) = dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) )
24	23	eleq2d	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑋 ∈ ( Fmla ‘ ∅ ) ↔ 𝑋 ∈ dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) ) )
25	24	biimpa	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → 𝑋 ∈ dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) )
26		eqid	⊢ ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) = ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 )
27	26	fviunfun	⊢ ( ( Fun ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ∧ ∅ ∈ ω ∧ 𝑋 ∈ dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) ) → ( ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ‘ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) ‘ 𝑋 ) )
28	17 19 25 27	syl3anc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ‘ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) ‘ 𝑋 ) )
29	11 28	eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) ‘ 𝑋 ) )
30		simpl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → 𝑀 ∈ 𝑉 )
31	6	adantr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V )
32		simpr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → 𝑋 ∈ ( Fmla ‘ ∅ ) )
33		eqid	⊢ ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) = ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) )
34	33	satfv0fvfmla0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )
35	30 31 32 34	syl3anc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )
36		elmapi	⊢ ( 𝑎 ∈ ( 𝑀 ↑_m ω ) → 𝑎 : ω ⟶ 𝑀 )
37		simpl	⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ) → 𝑎 : ω ⟶ 𝑀 )
38		fmla0xp	⊢ ( Fmla ‘ ∅ ) = ( { ∅ } × ( ω × ω ) )
39	38	eleq2i	⊢ ( 𝑋 ∈ ( Fmla ‘ ∅ ) ↔ 𝑋 ∈ ( { ∅ } × ( ω × ω ) ) )
40		elxp	⊢ ( 𝑋 ∈ ( { ∅ } × ( ω × ω ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) )
41	39 40	bitri	⊢ ( 𝑋 ∈ ( Fmla ‘ ∅ ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) )
42		xp1st	⊢ ( 𝑦 ∈ ( ω × ω ) → ( 1^st ‘ 𝑦 ) ∈ ω )
43	42	ad2antll	⊢ ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) → ( 1^st ‘ 𝑦 ) ∈ ω )
44		vex	⊢ 𝑥 ∈ V
45		vex	⊢ 𝑦 ∈ V
46	44 45	op2ndd	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑋 ) = 𝑦 )
47	46	fveq2d	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) = ( 1^st ‘ 𝑦 ) )
48	47	eleq1d	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω ↔ ( 1^st ‘ 𝑦 ) ∈ ω ) )
49	48	adantr	⊢ ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) → ( ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω ↔ ( 1^st ‘ 𝑦 ) ∈ ω ) )
50	43 49	mpbird	⊢ ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω )
51	50	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω )
52	41 51	sylbi	⊢ ( 𝑋 ∈ ( Fmla ‘ ∅ ) → ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω )
53	52	ad2antll	⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω )
54	37 53	ffvelcdmd	⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ) → ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 )
55		xp2nd	⊢ ( 𝑦 ∈ ( ω × ω ) → ( 2^nd ‘ 𝑦 ) ∈ ω )
56	55	ad2antll	⊢ ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ ω )
57	46	fveq2d	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑦 ) )
58	57	eleq1d	⊢ ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω ↔ ( 2^nd ‘ 𝑦 ) ∈ ω ) )
59	58	adantr	⊢ ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) → ( ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω ↔ ( 2^nd ‘ 𝑦 ) ∈ ω ) )
60	56 59	mpbird	⊢ ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) → ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω )
61	60	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ { ∅ } ∧ 𝑦 ∈ ( ω × ω ) ) ) → ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω )
62	41 61	sylbi	⊢ ( 𝑋 ∈ ( Fmla ‘ ∅ ) → ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω )
63	62	ad2antll	⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ) → ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ∈ ω )
64	37 63	ffvelcdmd	⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ) → ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 )
65	54 64	jca	⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ∧ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ) )
66	65	ex	⊢ ( 𝑎 : ω ⟶ 𝑀 → ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ∧ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ) ) )
67	36 66	syl	⊢ ( 𝑎 ∈ ( 𝑀 ↑_m ω ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ∧ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ) ) )
68	67	impcom	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ∧ 𝑎 ∈ ( 𝑀 ↑_m ω ) ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ∧ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ) )
69		brinxp	⊢ ( ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ∧ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) E ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ↔ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ) )
70	69	bicomd	⊢ ( ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ∧ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ 𝑀 ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ↔ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) E ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ) )
71	68 70	syl	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ∧ 𝑎 ∈ ( 𝑀 ↑_m ω ) ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ↔ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) E ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ) )
72		fvex	⊢ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ V
73	72	epeli	⊢ ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) E ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ↔ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) )
74	71 73	bitrdi	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) ∧ 𝑎 ∈ ( 𝑀 ↑_m ω ) ) → ( ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ↔ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) ) )
75	74	rabbidva	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )
76	35 75	eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ∅ ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )
77	29 76	eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )
78	1 77	eqtrd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ ( Fmla ‘ ∅ ) ) → ( 𝑀 Sat_∈ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑_m ω ) ∣ ( 𝑎 ‘ ( 1^st ‘ ( 2^nd ‘ 𝑋 ) ) ) ∈ ( 𝑎 ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑋 ) ) ) } )

Metamath Proof Explorer

Theorem satefvfmla0

Proof