This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem satfv1fvfmla1

Description: The value of the 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 satfv1fvfmla1 ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } )

Proof

Step Hyp Ref Expression
1 satfv1fvfmla1.x ⊢ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) )
2 simpl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝑀 ∈ 𝑉 )
3 simpr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝐸 ∈ 𝑊 )
4 1onn ⊢ 1o ∈ ω
5 4 a1i ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 1o ∈ ω )
6 2 3 5 3jca ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 1o ∈ ω ) )
7 6 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 1o ∈ ω ) )
8 satffun ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 1o ∈ ω ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) )
9 7 8 syl ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) )
10 simp2l ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐼 ∈ ω )
11 simp2r ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐽 ∈ ω )
12 simp3l ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐾 ∈ ω )
13 simp3r ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝐿 ∈ ω )
14 eqid ⊢ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) }
15 1 14 pm3.2i ⊢ ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } )
16 15 a1i ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) )
17 oveq1 ⊢ ( 𝑘 = 𝐾 → ( 𝑘 ∈𝑔 𝑙 ) = ( 𝐾 ∈𝑔 𝑙 ) )
18 17 oveq2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑙 ) ) )
19 18 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑙 ) ) ) )
20 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑎 ‘ 𝑘 ) = ( 𝑎 ‘ 𝐾 ) )
21 20 breq1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ↔ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) )
22 21 notbid ⊢ ( 𝑘 = 𝐾 → ( ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ↔ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) )
23 22 orbi2d ⊢ ( 𝑘 = 𝐾 → ( ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) ↔ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) ) )
24 23 rabbidv ⊢ ( 𝑘 = 𝐾 → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } )
25 24 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ↔ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
26 19 25 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ↔ ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
27 oveq2 ⊢ ( 𝑙 = 𝐿 → ( 𝐾 ∈𝑔 𝑙 ) = ( 𝐾 ∈𝑔 𝐿 ) )
28 27 oveq2d ⊢ ( 𝑙 = 𝐿 → ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑙 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) )
29 28 eqeq2d ⊢ ( 𝑙 = 𝐿 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑙 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ) )
30 fveq2 ⊢ ( 𝑙 = 𝐿 → ( 𝑎 ‘ 𝑙 ) = ( 𝑎 ‘ 𝐿 ) )
31 30 breq2d ⊢ ( 𝑙 = 𝐿 → ( ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ↔ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) )
32 31 notbid ⊢ ( 𝑙 = 𝐿 → ( ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ↔ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) )
33 32 orbi2d ⊢ ( 𝑙 = 𝐿 → ( ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) ↔ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) ) )
34 33 rabbidv ⊢ ( 𝑙 = 𝐿 → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } )
35 34 eqeq2d ⊢ ( 𝑙 = 𝐿 → ( { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ↔ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) )
36 29 35 anbi12d ⊢ ( 𝑙 = 𝐿 → ( ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ↔ ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) ) )
37 26 36 rspc2ev ⊢ ( ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ∧ ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝐾 ∈𝑔 𝐿 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
38 12 13 16 37 syl3anc ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
39 38 orcd ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝐽 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } ) ) )
40 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 ∈𝑔 𝑗 ) = ( 𝐼 ∈𝑔 𝑗 ) )
41 40 oveq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) )
42 41 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
43 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝑎 ‘ 𝑖 ) = ( 𝑎 ‘ 𝐼 ) )
44 43 breq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) )
45 44 notbid ⊢ ( 𝑖 = 𝐼 → ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ↔ ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) )
46 45 orbi1d ⊢ ( 𝑖 = 𝐼 → ( ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) ↔ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) ) )
47 46 rabbidv ⊢ ( 𝑖 = 𝐼 → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } )
48 47 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ↔ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
49 42 48 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ↔ ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
50 49 2rexbidv ⊢ ( 𝑖 = 𝐼 → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
51 eqidd ⊢ ( 𝑖 = 𝐼 → 𝑛 = 𝑛 )
52 51 40 goaleq12d ⊢ ( 𝑖 = 𝐼 → ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) )
53 52 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) ) )
54 eqeq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 = 𝑛 ↔ 𝐼 = 𝑛 ) )
55 biidd ⊢ ( 𝑖 = 𝐼 → ( if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) ↔ if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) )
56 43 breq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 ) )
57 56 44 ifpbi23d ⊢ ( 𝑖 = 𝐼 → ( if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ↔ if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) )
58 54 55 57 ifpbi123d ⊢ ( 𝑖 = 𝐼 → ( if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) ↔ if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) ) )
59 58 ralbidv ⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) ↔ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) ) )
60 59 rabbidv ⊢ ( 𝑖 = 𝐼 → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } )
61 60 eqeq2d ⊢ ( 𝑖 = 𝐼 → ( { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ↔ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) )
62 53 61 anbi12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ↔ ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
63 62 rexbidv ⊢ ( 𝑖 = 𝐼 → ( ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ↔ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
64 50 63 orbi12d ⊢ ( 𝑖 = 𝐼 → ( ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ↔ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
65 oveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝐼 ∈𝑔 𝑗 ) = ( 𝐼 ∈𝑔 𝐽 ) )
66 65 oveq1d ⊢ ( 𝑗 = 𝐽 → ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) )
67 66 eqeq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
68 fveq2 ⊢ ( 𝑗 = 𝐽 → ( 𝑎 ‘ 𝑗 ) = ( 𝑎 ‘ 𝐽 ) )
69 68 breq2d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) )
70 69 notbid ⊢ ( 𝑗 = 𝐽 → ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ↔ ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) )
71 70 orbi1d ⊢ ( 𝑗 = 𝐽 → ( ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) ↔ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) ) )
72 71 rabbidv ⊢ ( 𝑗 = 𝐽 → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } )
73 72 eqeq2d ⊢ ( 𝑗 = 𝐽 → ( { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ↔ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
74 67 73 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ↔ ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
75 74 2rexbidv ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
76 eqidd ⊢ ( 𝑗 = 𝐽 → 𝑛 = 𝑛 )
77 76 65 goaleq12d ⊢ ( 𝑗 = 𝐽 → ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝐽 ) )
78 77 eqeq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝐽 ) ) )
79 eqeq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 = 𝑛 ↔ 𝐽 = 𝑛 ) )
80 biidd ⊢ ( 𝑗 = 𝐽 → ( 𝑧 𝐸 𝑧 ↔ 𝑧 𝐸 𝑧 ) )
81 68 breq2d ⊢ ( 𝑗 = 𝐽 → ( 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ↔ 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) )
82 79 80 81 ifpbi123d ⊢ ( 𝑗 = 𝐽 → ( if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) ↔ if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
83 biidd ⊢ ( 𝑗 = 𝐽 → ( ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 ↔ ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 ) )
84 79 83 69 ifpbi123d ⊢ ( 𝑗 = 𝐽 → ( if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ↔ if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) )
85 82 84 ifpbi23d ⊢ ( 𝑗 = 𝐽 → ( if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) ↔ if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
86 85 ralbidv ⊢ ( 𝑗 = 𝐽 → ( ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) ↔ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) ) )
87 86 rabbidv ⊢ ( 𝑗 = 𝐽 → { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } )
88 87 eqeq2d ⊢ ( 𝑗 = 𝐽 → ( { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ↔ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } ) )
89 78 88 anbi12d ⊢ ( 𝑗 = 𝐽 → ( ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ↔ ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝐽 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } ) ) )
90 89 rexbidv ⊢ ( 𝑗 = 𝐽 → ( ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ↔ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝐽 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } ) ) )
91 75 90 orbi12d ⊢ ( 𝑗 = 𝐽 → ( ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ↔ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝐽 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } ) ) ) )
92 64 91 rspc2ev ⊢ ( ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝐼 ∈𝑔 𝐽 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝐼 ∈𝑔 𝐽 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝐼 = 𝑛 , if- ( 𝐽 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝐽 ) ) , if- ( 𝐽 = 𝑛 , ( 𝑎 ‘ 𝐼 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ) ) } ) ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
93 10 11 39 92 syl3anc ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
94 1 ovexi ⊢ 𝑋 ∈ V
95 94 a1i ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → 𝑋 ∈ V )
96 ovex ⊢ ( 𝑀 ↑m ω ) ∈ V
97 96 rabex ⊢ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ∈ V
98 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ↔ 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ) )
99 eqeq1 ⊢ ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ↔ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) )
100 98 99 bi2anan9 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) → ( ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ↔ ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
101 100 2rexbidv ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) → ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ) )
102 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ) )
103 eqeq1 ⊢ ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } → ( 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ↔ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) )
104 102 103 bi2anan9 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) → ( ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ↔ ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
105 104 rexbidv ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) → ( ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ↔ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) )
106 101 105 orbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) → ( ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ↔ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
107 106 2rexbidv ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
108 107 opelopabga ⊢ ( ( 𝑋 ∈ V ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ∈ V ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
109 95 97 108 sylancl ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑋 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑋 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) ) )
110 93 109 mpbird ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } )
111 110 olcd ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∨ ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) )
112 elun ⊢ ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) ↔ ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∨ ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) )
113 111 112 sylibr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) )
114 eqid ⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
115 114 satfv1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) )
116 115 eleq2d ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) ↔ ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) ) )
117 116 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) ↔ ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( ( 𝑖 ∈𝑔 𝑗 ) ⊼𝑔 ( 𝑘 ∈𝑔 𝑙 ) ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ∨ ¬ ( 𝑎 ‘ 𝑘 ) 𝐸 ( 𝑎 ‘ 𝑙 ) ) } ) ∨ ∃ 𝑛 ∈ ω ( 𝑥 = ∀𝑔 𝑛 ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 if- ( 𝑖 = 𝑛 , if- ( 𝑗 = 𝑛 , 𝑧 𝐸 𝑧 , 𝑧 𝐸 ( 𝑎 ‘ 𝑗 ) ) , if- ( 𝑗 = 𝑛 , ( 𝑎 ‘ 𝑖 ) 𝐸 𝑧 , ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) ) ) } ) ) } ) ) )
118 113 117 mpbird ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) )
119 funopfv ⊢ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) → ( ⟨ 𝑋 , { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ⟩ ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } ) )
120 9 118 119 sylc ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐼 ∈ ω ∧ 𝐽 ∈ ω ) ∧ ( 𝐾 ∈ ω ∧ 𝐿 ∈ ω ) ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ 1o ) ‘ 𝑋 ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐼 ) 𝐸 ( 𝑎 ‘ 𝐽 ) ∨ ¬ ( 𝑎 ‘ 𝐾 ) 𝐸 ( 𝑎 ‘ 𝐿 ) ) } )