Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝑀 ∈ 𝑉 ) |
2 |
|
3simpc |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) |
3 |
|
pm3.22 |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) ) |
4 |
3
|
3adant1 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) ) |
5 |
|
eqid |
⊢ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) = ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) |
6 |
5
|
satefvfmla1 |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) ) → ( 𝑀 Sat∈ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐴 ) ∈ ( 𝑎 ‘ 𝐵 ) ∨ ¬ ( 𝑎 ‘ 𝐵 ) ∈ ( 𝑎 ‘ 𝐴 ) ) } ) |
7 |
1 2 4 6
|
syl3anc |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑀 Sat∈ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ) = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐴 ) ∈ ( 𝑎 ‘ 𝐵 ) ∨ ¬ ( 𝑎 ‘ 𝐵 ) ∈ ( 𝑎 ‘ 𝐴 ) ) } ) |
8 |
|
elnanel |
⊢ ( ( 𝑎 ‘ 𝐴 ) ∈ ( 𝑎 ‘ 𝐵 ) ⊼ ( 𝑎 ‘ 𝐵 ) ∈ ( 𝑎 ‘ 𝐴 ) ) |
9 |
|
nanor |
⊢ ( ( ( 𝑎 ‘ 𝐴 ) ∈ ( 𝑎 ‘ 𝐵 ) ⊼ ( 𝑎 ‘ 𝐵 ) ∈ ( 𝑎 ‘ 𝐴 ) ) ↔ ( ¬ ( 𝑎 ‘ 𝐴 ) ∈ ( 𝑎 ‘ 𝐵 ) ∨ ¬ ( 𝑎 ‘ 𝐵 ) ∈ ( 𝑎 ‘ 𝐴 ) ) ) |
10 |
8 9
|
mpbi |
⊢ ( ¬ ( 𝑎 ‘ 𝐴 ) ∈ ( 𝑎 ‘ 𝐵 ) ∨ ¬ ( 𝑎 ‘ 𝐵 ) ∈ ( 𝑎 ‘ 𝐴 ) ) |
11 |
10
|
a1i |
⊢ ( 𝑎 ∈ ( 𝑀 ↑m ω ) → ( ¬ ( 𝑎 ‘ 𝐴 ) ∈ ( 𝑎 ‘ 𝐵 ) ∨ ¬ ( 𝑎 ‘ 𝐵 ) ∈ ( 𝑎 ‘ 𝐴 ) ) ) |
12 |
11
|
rabeqc |
⊢ { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( ¬ ( 𝑎 ‘ 𝐴 ) ∈ ( 𝑎 ‘ 𝐵 ) ∨ ¬ ( 𝑎 ‘ 𝐵 ) ∈ ( 𝑎 ‘ 𝐴 ) ) } = ( 𝑀 ↑m ω ) |
13 |
7 12
|
eqtrdi |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑀 Sat∈ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ) = ( 𝑀 ↑m ω ) ) |
14 |
|
ovex |
⊢ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ∈ V |
15 |
|
prv |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ∈ V ) → ( 𝑀 ⊧ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ↔ ( 𝑀 Sat∈ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ) = ( 𝑀 ↑m ω ) ) ) |
16 |
1 14 15
|
sylancl |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝑀 ⊧ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ↔ ( 𝑀 Sat∈ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ) = ( 𝑀 ↑m ω ) ) ) |
17 |
13 16
|
mpbird |
⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → 𝑀 ⊧ ( ( 𝐴 ∈𝑔 𝐵 ) ⊼𝑔 ( 𝐵 ∈𝑔 𝐴 ) ) ) |