Step |
Hyp |
Ref |
Expression |
1 |
|
1n0 |
⊢ 1o ≠ ∅ |
2 |
1
|
neii |
⊢ ¬ 1o = ∅ |
3 |
2
|
intnanr |
⊢ ¬ ( 1o = ∅ ∧ 〈 𝐴 , 𝐵 〉 = 〈 𝑖 , 𝑗 〉 ) |
4 |
|
1oex |
⊢ 1o ∈ V |
5 |
|
opex |
⊢ 〈 𝐴 , 𝐵 〉 ∈ V |
6 |
4 5
|
opth |
⊢ ( 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = 〈 ∅ , 〈 𝑖 , 𝑗 〉 〉 ↔ ( 1o = ∅ ∧ 〈 𝐴 , 𝐵 〉 = 〈 𝑖 , 𝑗 〉 ) ) |
7 |
3 6
|
mtbir |
⊢ ¬ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = 〈 ∅ , 〈 𝑖 , 𝑗 〉 〉 |
8 |
|
goel |
⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 𝑖 ∈𝑔 𝑗 ) = 〈 ∅ , 〈 𝑖 , 𝑗 〉 〉 ) |
9 |
8
|
eqeq2d |
⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ( 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = 〈 ∅ , 〈 𝑖 , 𝑗 〉 〉 ) ) |
10 |
7 9
|
mtbiri |
⊢ ( ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) → ¬ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) ) |
11 |
10
|
rgen2 |
⊢ ∀ 𝑖 ∈ ω ∀ 𝑗 ∈ ω ¬ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) |
12 |
|
ralnex2 |
⊢ ( ∀ 𝑖 ∈ ω ∀ 𝑗 ∈ ω ¬ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ¬ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) ) |
13 |
11 12
|
mpbi |
⊢ ¬ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) |
14 |
13
|
intnan |
⊢ ¬ ( 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) ) |
15 |
|
eqeq1 |
⊢ ( 𝑥 = 〈 1o , 〈 𝐴 , 𝐵 〉 〉 → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) ) ) |
16 |
15
|
2rexbidv |
⊢ ( 𝑥 = 〈 1o , 〈 𝐴 , 𝐵 〉 〉 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) ) ) |
17 |
|
fmla0 |
⊢ ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) } |
18 |
16 17
|
elrab2 |
⊢ ( 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ∈ ( Fmla ‘ ∅ ) ↔ ( 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ∈ V ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 〈 1o , 〈 𝐴 , 𝐵 〉 〉 = ( 𝑖 ∈𝑔 𝑗 ) ) ) |
19 |
14 18
|
mtbir |
⊢ ¬ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ∈ ( Fmla ‘ ∅ ) |
20 |
|
gonafv |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ⊼𝑔 𝐵 ) = 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ) |
21 |
20
|
eleq1d |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ↔ 〈 1o , 〈 𝐴 , 𝐵 〉 〉 ∈ ( Fmla ‘ ∅ ) ) ) |
22 |
19 21
|
mtbiri |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ) |
23 |
|
eqid |
⊢ ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) = ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) |
24 |
23
|
dmmptss |
⊢ dom ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) ⊆ ( V × V ) |
25 |
|
relxp |
⊢ Rel ( V × V ) |
26 |
|
relss |
⊢ ( dom ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) ⊆ ( V × V ) → ( Rel ( V × V ) → Rel dom ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) ) ) |
27 |
24 25 26
|
mp2 |
⊢ Rel dom ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) |
28 |
|
df-gona |
⊢ ⊼𝑔 = ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) |
29 |
28
|
dmeqi |
⊢ dom ⊼𝑔 = dom ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) |
30 |
29
|
releqi |
⊢ ( Rel dom ⊼𝑔 ↔ Rel dom ( 𝑥 ∈ ( V × V ) ↦ 〈 1o , 𝑥 〉 ) ) |
31 |
27 30
|
mpbir |
⊢ Rel dom ⊼𝑔 |
32 |
31
|
ovprc |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ⊼𝑔 𝐵 ) = ∅ ) |
33 |
|
peano1 |
⊢ ∅ ∈ ω |
34 |
|
fmlaomn0 |
⊢ ( ∅ ∈ ω → ∅ ∉ ( Fmla ‘ ∅ ) ) |
35 |
33 34
|
ax-mp |
⊢ ∅ ∉ ( Fmla ‘ ∅ ) |
36 |
35
|
neli |
⊢ ¬ ∅ ∈ ( Fmla ‘ ∅ ) |
37 |
|
eleq1 |
⊢ ( ( 𝐴 ⊼𝑔 𝐵 ) = ∅ → ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ↔ ∅ ∈ ( Fmla ‘ ∅ ) ) ) |
38 |
36 37
|
mtbiri |
⊢ ( ( 𝐴 ⊼𝑔 𝐵 ) = ∅ → ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ) |
39 |
32 38
|
syl |
⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ) |
40 |
22 39
|
pm2.61i |
⊢ ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) |
41 |
|
fveq2 |
⊢ ( 𝑁 = ∅ → ( Fmla ‘ 𝑁 ) = ( Fmla ‘ ∅ ) ) |
42 |
41
|
eleq2d |
⊢ ( 𝑁 = ∅ → ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ 𝑁 ) ↔ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ ∅ ) ) ) |
43 |
40 42
|
mtbiri |
⊢ ( 𝑁 = ∅ → ¬ ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ 𝑁 ) ) |
44 |
43
|
necon2ai |
⊢ ( ( 𝐴 ⊼𝑔 𝐵 ) ∈ ( Fmla ‘ 𝑁 ) → 𝑁 ≠ ∅ ) |