Step | Hyp | Ref
| Expression |
1 | | 1n0 8150 |
. . . . . . . . . . . . 13
⊢
1o ≠ ∅ |
2 | 1 | neii 2936 |
. . . . . . . . . . . 12
⊢ ¬
1o = ∅ |
3 | 2 | intnanr 491 |
. . . . . . . . . . 11
⊢ ¬
(1o = ∅ ∧ 〈𝐴, 𝐵〉 = 〈𝑖, 𝑗〉) |
4 | | 1oex 8144 |
. . . . . . . . . . . 12
⊢
1o ∈ V |
5 | | opex 5322 |
. . . . . . . . . . . 12
⊢
〈𝐴, 𝐵〉 ∈ V |
6 | 4, 5 | opth 5334 |
. . . . . . . . . . 11
⊢
(〈1o, 〈𝐴, 𝐵〉〉 = 〈∅, 〈𝑖, 𝑗〉〉 ↔ (1o = ∅
∧ 〈𝐴, 𝐵〉 = 〈𝑖, 𝑗〉)) |
7 | 3, 6 | mtbir 326 |
. . . . . . . . . 10
⊢ ¬
〈1o, 〈𝐴, 𝐵〉〉 = 〈∅, 〈𝑖, 𝑗〉〉 |
8 | | goel 32880 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = 〈∅, 〈𝑖, 𝑗〉〉) |
9 | 8 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
(〈1o, 〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗) ↔ 〈1o, 〈𝐴, 𝐵〉〉 = 〈∅, 〈𝑖, 𝑗〉〉)) |
10 | 7, 9 | mtbiri 330 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ¬
〈1o, 〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗)) |
11 | 10 | rgen2 3115 |
. . . . . . . 8
⊢
∀𝑖 ∈
ω ∀𝑗 ∈
ω ¬ 〈1o, 〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗) |
12 | | ralnex2 3172 |
. . . . . . . 8
⊢
(∀𝑖 ∈
ω ∀𝑗 ∈
ω ¬ 〈1o, 〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗) ↔ ¬ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 〈1o,
〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗)) |
13 | 11, 12 | mpbi 233 |
. . . . . . 7
⊢ ¬
∃𝑖 ∈ ω
∃𝑗 ∈ ω
〈1o, 〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗) |
14 | 13 | intnan 490 |
. . . . . 6
⊢ ¬
(〈1o, 〈𝐴, 𝐵〉〉 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω
〈1o, 〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗)) |
15 | | eqeq1 2742 |
. . . . . . . 8
⊢ (𝑥 = 〈1o,
〈𝐴, 𝐵〉〉 → (𝑥 = (𝑖∈𝑔𝑗) ↔ 〈1o, 〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗))) |
16 | 15 | 2rexbidv 3210 |
. . . . . . 7
⊢ (𝑥 = 〈1o,
〈𝐴, 𝐵〉〉 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 〈1o,
〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗))) |
17 | | fmla0 32915 |
. . . . . . 7
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} |
18 | 16, 17 | elrab2 3591 |
. . . . . 6
⊢
(〈1o, 〈𝐴, 𝐵〉〉 ∈ (Fmla‘∅)
↔ (〈1o, 〈𝐴, 𝐵〉〉 ∈ V ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω
〈1o, 〈𝐴, 𝐵〉〉 = (𝑖∈𝑔𝑗))) |
19 | 14, 18 | mtbir 326 |
. . . . 5
⊢ ¬
〈1o, 〈𝐴, 𝐵〉〉 ∈
(Fmla‘∅) |
20 | | gonafv 32883 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴⊼𝑔𝐵) = 〈1o,
〈𝐴, 𝐵〉〉) |
21 | 20 | eleq1d 2817 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴⊼𝑔𝐵) ∈ (Fmla‘∅)
↔ 〈1o, 〈𝐴, 𝐵〉〉 ∈
(Fmla‘∅))) |
22 | 19, 21 | mtbiri 330 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ¬ (𝐴⊼𝑔𝐵) ∈
(Fmla‘∅)) |
23 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑥 ∈ (V × V) ↦
〈1o, 𝑥〉) = (𝑥 ∈ (V × V) ↦
〈1o, 𝑥〉) |
24 | 23 | dmmptss 6073 |
. . . . . . . 8
⊢ dom
(𝑥 ∈ (V × V)
↦ 〈1o, 𝑥〉) ⊆ (V ×
V) |
25 | | relxp 5543 |
. . . . . . . 8
⊢ Rel (V
× V) |
26 | | relss 5627 |
. . . . . . . 8
⊢ (dom
(𝑥 ∈ (V × V)
↦ 〈1o, 𝑥〉) ⊆ (V × V) → (Rel (V
× V) → Rel dom (𝑥 ∈ (V × V) ↦
〈1o, 𝑥〉))) |
27 | 24, 25, 26 | mp2 9 |
. . . . . . 7
⊢ Rel dom
(𝑥 ∈ (V × V)
↦ 〈1o, 𝑥〉) |
28 | | df-gona 32874 |
. . . . . . . . 9
⊢
⊼𝑔 = (𝑥 ∈ (V × V) ↦
〈1o, 𝑥〉) |
29 | 28 | dmeqi 5747 |
. . . . . . . 8
⊢ dom
⊼𝑔 = dom (𝑥 ∈ (V × V) ↦
〈1o, 𝑥〉) |
30 | 29 | releqi 5623 |
. . . . . . 7
⊢ (Rel dom
⊼𝑔 ↔ Rel dom (𝑥 ∈ (V × V) ↦
〈1o, 𝑥〉)) |
31 | 27, 30 | mpbir 234 |
. . . . . 6
⊢ Rel dom
⊼𝑔 |
32 | 31 | ovprc 7208 |
. . . . 5
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴⊼𝑔𝐵) = ∅) |
33 | | peano1 7620 |
. . . . . . . 8
⊢ ∅
∈ ω |
34 | | fmlaomn0 32923 |
. . . . . . . 8
⊢ (∅
∈ ω → ∅ ∉ (Fmla‘∅)) |
35 | 33, 34 | ax-mp 5 |
. . . . . . 7
⊢ ∅
∉ (Fmla‘∅) |
36 | 35 | neli 3040 |
. . . . . 6
⊢ ¬
∅ ∈ (Fmla‘∅) |
37 | | eleq1 2820 |
. . . . . 6
⊢ ((𝐴⊼𝑔𝐵) = ∅ → ((𝐴⊼𝑔𝐵) ∈ (Fmla‘∅)
↔ ∅ ∈ (Fmla‘∅))) |
38 | 36, 37 | mtbiri 330 |
. . . . 5
⊢ ((𝐴⊼𝑔𝐵) = ∅ → ¬ (𝐴⊼𝑔𝐵) ∈
(Fmla‘∅)) |
39 | 32, 38 | syl 17 |
. . . 4
⊢ (¬
(𝐴 ∈ V ∧ 𝐵 ∈ V) → ¬ (𝐴⊼𝑔𝐵) ∈
(Fmla‘∅)) |
40 | 22, 39 | pm2.61i 185 |
. . 3
⊢ ¬
(𝐴⊼𝑔𝐵) ∈
(Fmla‘∅) |
41 | | fveq2 6674 |
. . . 4
⊢ (𝑁 = ∅ →
(Fmla‘𝑁) =
(Fmla‘∅)) |
42 | 41 | eleq2d 2818 |
. . 3
⊢ (𝑁 = ∅ → ((𝐴⊼𝑔𝐵) ∈ (Fmla‘𝑁) ↔ (𝐴⊼𝑔𝐵) ∈
(Fmla‘∅))) |
43 | 40, 42 | mtbiri 330 |
. 2
⊢ (𝑁 = ∅ → ¬ (𝐴⊼𝑔𝐵) ∈ (Fmla‘𝑁)) |
44 | 43 | necon2ai 2963 |
1
⊢ ((𝐴⊼𝑔𝐵) ∈ (Fmla‘𝑁) → 𝑁 ≠ ∅) |