Metamath Proof Explorer

Theorem satefvfmla1

Description: The simplified satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023)

Ref Expression
Hypothesis satfv1fvfmla1.x ⊢ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) )
Assertion satefvfmla1 ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑀 Sat∈ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) ) } )

Proof

Step Hyp Ref Expression
1 satfv1fvfmla1.x ⊢ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) )
2 1 ovexi ⊢ 𝑋 ∈ V
3 2 jctr ⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ V ) )
4 3 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ V ) )
5 satefv ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑋 ∈ V ) → ( 𝑀 Sat∈ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑋 ) )
6 4 5 syl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑀 Sat∈ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑋 ) )
7 sqxpexg ⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 × 𝑀 ) ∈ V )
8 inex2g ⊢ ( ( 𝑀 × 𝑀 ) ∈ V → ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V )
9 7 8 syl ⊢ ( 𝑀 ∈ 𝑉 → ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V )
10 9 ancli ⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) )
11 10 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) )
12 satom ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) → ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) = ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) )
13 11 12 syl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) = ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) )
14 13 fveq1d ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑋 ) = ( ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ‘ 𝑋 ) )
15 satfun ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) → ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀 ↑m ω ) )
16 11 15 syl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀 ↑m ω ) )
17 16 ffund ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → Fun ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) )
18 13 eqcomd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) = ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) )
19 18 funeqd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( Fun ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ↔ Fun ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ) )
20 17 19 mpbird ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → Fun ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) )
21 1onn ⊢ 1o ∈ ω
22 21 a1i ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 1o ∈ ω )
23 1 2goelgoanfmla1 ⊢ ( ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ ( Fmla ‘ 1o ) )
24 23 3adant1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ ( Fmla ‘ 1o ) )
25 21 a1i ⊢ ( 𝑀 ∈ 𝑉 → 1o ∈ ω )
26 satfdmfmla ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ∧ 1o ∈ ω ) → dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) = ( Fmla ‘ 1o ) )
27 9 25 26 mpd3an23 ⊢ ( 𝑀 ∈ 𝑉 → dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) = ( Fmla ‘ 1o ) )
28 27 3ad2ant1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) = ( Fmla ‘ 1o ) )
29 24 28 eleqtrrd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) )
30 eqid ⊢ ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) = ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 )
31 30 fviunfun ⊢ ( ( Fun ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ∧ 1o ∈ ω ∧ 𝑋 ∈ dom ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) ) → ( ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ‘ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) ‘ 𝑋 ) )
32 20 22 29 31 syl3anc ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ∪ 𝑖 ∈ ω ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 𝑖 ) ‘ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) ‘ 𝑋 ) )
33 14 32 eqtrd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ ω ) ‘ 𝑋 ) = ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) ‘ 𝑋 ) )
34 1 satfv1fvfmla1 ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( E ∩ ( 𝑀 × 𝑀 ) ) ∈ V ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐿 ) ) } )
35 10 34 syl3an1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐿 ) ) } )
36 brin ⊢ ( ( 𝑎 ‘ 𝐼 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐽 ) ↔ ( ( 𝑎 ‘ 𝐼 ) E ( 𝑎 ‘ 𝐽 ) ∧ ( 𝑎 ‘ 𝐼 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐽 ) ) )
37 elmapi ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → 𝑎 : ω ⟶ 𝑀 )
38 ffvelrn ⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ 𝐼 ∈ ω ) → ( 𝑎 ‘ 𝐼 ) ∈ 𝑀 )
39 38 ex ⊢ ( 𝑎 : ω ⟶ 𝑀 → ( 𝐼 ∈ ω → ( 𝑎 ‘ 𝐼 ) ∈ 𝑀 ) )
40 37 39 syl ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( 𝐼 ∈ ω → ( 𝑎 ‘ 𝐼 ) ∈ 𝑀 ) )
41 ffvelrn ⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ 𝐽 ∈ ω ) → ( 𝑎 ‘ 𝐽 ) ∈ 𝑀 )
42 41 ex ⊢ ( 𝑎 : ω ⟶ 𝑀 → ( 𝐽 ∈ ω → ( 𝑎 ‘ 𝐽 ) ∈ 𝑀 ) )
43 37 42 syl ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( 𝐽 ∈ ω → ( 𝑎 ‘ 𝐽 ) ∈ 𝑀 ) )
44 40 43 anim12d ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( ( 𝑎 ‘ 𝐼 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐽 ) ∈ 𝑀 ) ) )
45 44 com12 ⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) → ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ( 𝑎 ‘ 𝐼 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐽 ) ∈ 𝑀 ) ) )
46 45 3ad2ant2 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ( 𝑎 ‘ 𝐼 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐽 ) ∈ 𝑀 ) ) )
47 46 imp ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( 𝑎 ‘ 𝐼 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐽 ) ∈ 𝑀 ) )
48 brxp ⊢ ( ( 𝑎 ‘ 𝐼 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐽 ) ↔ ( ( 𝑎 ‘ 𝐼 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐽 ) ∈ 𝑀 ) )
49 47 48 sylibr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( 𝑎 ‘ 𝐼 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐽 ) )
50 49 biantrud ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( 𝑎 ‘ 𝐼 ) E ( 𝑎 ‘ 𝐽 ) ↔ ( ( 𝑎 ‘ 𝐼 ) E ( 𝑎 ‘ 𝐽 ) ∧ ( 𝑎 ‘ 𝐼 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐽 ) ) ) )
51 fvex ⊢ ( 𝑎 ‘ 𝐽 ) ∈ V
52 51 epeli ⊢ ( ( 𝑎 ‘ 𝐼 ) E ( 𝑎 ‘ 𝐽 ) ↔ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) )
53 50 52 bitr3di ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( ( 𝑎 ‘ 𝐼 ) E ( 𝑎 ‘ 𝐽 ) ∧ ( 𝑎 ‘ 𝐼 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐽 ) ) ↔ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) ) )
54 36 53 syl5bb ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( 𝑎 ‘ 𝐼 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐽 ) ↔ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) ) )
55 54 notbid ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ¬ ( 𝑎 ‘ 𝐼 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐽 ) ↔ ¬ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) ) )
56 brin ⊢ ( ( 𝑎 ‘ 𝐾 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐿 ) ↔ ( ( 𝑎 ‘ 𝐾 ) E ( 𝑎 ‘ 𝐿 ) ∧ ( 𝑎 ‘ 𝐾 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐿 ) ) )
57 ffvelrn ⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ 𝐾 ∈ ω ) → ( 𝑎 ‘ 𝐾 ) ∈ 𝑀 )
58 57 ex ⊢ ( 𝑎 : ω ⟶ 𝑀 → ( 𝐾 ∈ ω → ( 𝑎 ‘ 𝐾 ) ∈ 𝑀 ) )
59 37 58 syl ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( 𝐾 ∈ ω → ( 𝑎 ‘ 𝐾 ) ∈ 𝑀 ) )
60 ffvelrn ⊢ ( ( 𝑎 : ω ⟶ 𝑀 ∧ 𝐿 ∈ ω ) → ( 𝑎 ‘ 𝐿 ) ∈ 𝑀 )
61 60 ex ⊢ ( 𝑎 : ω ⟶ 𝑀 → ( 𝐿 ∈ ω → ( 𝑎 ‘ 𝐿 ) ∈ 𝑀 ) )
62 37 61 syl ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( 𝐿 ∈ ω → ( 𝑎 ‘ 𝐿 ) ∈ 𝑀 ) )
63 59 62 anim12d ⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) → ( ( 𝑎 ‘ 𝐾 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐿 ) ∈ 𝑀 ) ) )
64 63 com12 ⊢ ( ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) → ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ( 𝑎 ‘ 𝐾 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐿 ) ∈ 𝑀 ) ) )
65 64 3ad2ant3 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ( 𝑎 ‘ 𝐾 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐿 ) ∈ 𝑀 ) ) )
66 65 imp ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( 𝑎 ‘ 𝐾 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐿 ) ∈ 𝑀 ) )
67 brxp ⊢ ( ( 𝑎 ‘ 𝐾 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐿 ) ↔ ( ( 𝑎 ‘ 𝐾 ) ∈ 𝑀 ∧ ( 𝑎 ‘ 𝐿 ) ∈ 𝑀 ) )
68 66 67 sylibr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( 𝑎 ‘ 𝐾 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐿 ) )
69 68 biantrud ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( 𝑎 ‘ 𝐾 ) E ( 𝑎 ‘ 𝐿 ) ↔ ( ( 𝑎 ‘ 𝐾 ) E ( 𝑎 ‘ 𝐿 ) ∧ ( 𝑎 ‘ 𝐾 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐿 ) ) ) )
70 fvex ⊢ ( 𝑎 ‘ 𝐿 ) ∈ V
71 70 epeli ⊢ ( ( 𝑎 ‘ 𝐾 ) E ( 𝑎 ‘ 𝐿 ) ↔ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) )
72 69 71 bitr3di ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( ( 𝑎 ‘ 𝐾 ) E ( 𝑎 ‘ 𝐿 ) ∧ ( 𝑎 ‘ 𝐾 ) ( 𝑀 × 𝑀 ) ( 𝑎 ‘ 𝐿 ) ) ↔ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) ) )
73 56 72 syl5bb ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( 𝑎 ‘ 𝐾 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐿 ) ↔ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) ) )
74 73 notbid ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ¬ ( 𝑎 ‘ 𝐾 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐿 ) ↔ ¬ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) ) )
75 55 74 orbi12d ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) ∧ 𝑎 ∈ ( 𝑀 ↑m ω ) ) → ( ( ¬ ( 𝑎 ‘ 𝐼 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐿 ) ) ↔ ( ¬ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) ) ) )
76 75 rabbidva ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ( E ∩ ( 𝑀 × 𝑀 ) ) ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) ) } )
77 35 76 eqtrd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( ( 𝑀 Sat ( E ∩ ( 𝑀 × 𝑀 ) ) ) ‘ 1o ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) ) } )
78 6 33 77 3eqtrd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑀 Sat∈ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) ∈ ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) ∈ ( 𝑎 ‘ 𝐿 ) ) } )