Step | Hyp | Ref
| Expression |
1 | | fmla0 33057 |
. 2
⊢
(Fmla‘∅) = {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} |
2 | | rabab 3436 |
. 2
⊢ {𝑥 ∈ V ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} = {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} |
3 | | abeq1 2870 |
. . 3
⊢ ({𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} = ({∅} × (ω ×
ω)) ↔ ∀𝑥(∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗) ↔ 𝑥 ∈ ({∅} × (ω ×
ω)))) |
4 | | goel 33022 |
. . . . . 6
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖∈𝑔𝑗) = 〈∅, 〈𝑖, 𝑗〉〉) |
5 | 4 | eqeq2d 2748 |
. . . . 5
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑥 = (𝑖∈𝑔𝑗) ↔ 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉)) |
6 | 5 | 2rexbiia 3217 |
. . . 4
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉) |
7 | | 0ex 5200 |
. . . . . . . . . 10
⊢ ∅
∈ V |
8 | 7 | snid 4577 |
. . . . . . . . 9
⊢ ∅
∈ {∅} |
9 | 8 | a1i 11 |
. . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → ∅
∈ {∅}) |
10 | | opelxpi 5588 |
. . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
〈𝑖, 𝑗〉 ∈ (ω ×
ω)) |
11 | 9, 10 | opelxpd 5589 |
. . . . . . 7
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) →
〈∅, 〈𝑖,
𝑗〉〉 ∈
({∅} × (ω × ω))) |
12 | | eleq1 2825 |
. . . . . . 7
⊢ (𝑥 = 〈∅, 〈𝑖, 𝑗〉〉 → (𝑥 ∈ ({∅} × (ω ×
ω)) ↔ 〈∅, 〈𝑖, 𝑗〉〉 ∈ ({∅} ×
(ω × ω)))) |
13 | 11, 12 | syl5ibrcom 250 |
. . . . . 6
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑥 = 〈∅, 〈𝑖, 𝑗〉〉 → 𝑥 ∈ ({∅} × (ω ×
ω)))) |
14 | 13 | rexlimivv 3211 |
. . . . 5
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = 〈∅,
〈𝑖, 𝑗〉〉 → 𝑥 ∈ ({∅} × (ω ×
ω))) |
15 | | elxpi 5573 |
. . . . . 6
⊢ (𝑥 ∈ ({∅} ×
(ω × ω)) → ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ {∅} ∧ 𝑧 ∈ (ω ×
ω)))) |
16 | | elsni 4558 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {∅} → 𝑦 = ∅) |
17 | 16 | opeq1d 4790 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {∅} →
〈𝑦, 𝑧〉 = 〈∅, 𝑧〉) |
18 | 17 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {∅} → (𝑥 = 〈𝑦, 𝑧〉 ↔ 𝑥 = 〈∅, 𝑧〉)) |
19 | 18 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑦 ∈ {∅} ∧ 𝑧 ∈ (ω ×
ω)) → (𝑥 =
〈𝑦, 𝑧〉 ↔ 𝑥 = 〈∅, 𝑧〉)) |
20 | | elxpi 5573 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (ω ×
ω) → ∃𝑖∃𝑗(𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω))) |
21 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 〈∅, 𝑧〉 ∧ (𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω))) → (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) |
22 | | simpl 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 〈∅, 𝑧〉 ∧ (𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω))) → 𝑥 = 〈∅, 𝑧〉) |
23 | | opeq2 4785 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑖, 𝑗〉 → 〈∅, 𝑧〉 = 〈∅,
〈𝑖, 𝑗〉〉) |
24 | 23 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → 〈∅, 𝑧〉 = 〈∅,
〈𝑖, 𝑗〉〉) |
25 | 24 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 〈∅, 𝑧〉 ∧ (𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω))) → 〈∅,
𝑧〉 = 〈∅,
〈𝑖, 𝑗〉〉) |
26 | 22, 25 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 〈∅, 𝑧〉 ∧ (𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω))) → 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉) |
27 | 21, 26 | jca 515 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 〈∅, 𝑧〉 ∧ (𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω))) → ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉)) |
28 | 27 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈∅, 𝑧〉 → ((𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉))) |
29 | 28 | 2eximdv 1927 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈∅, 𝑧〉 → (∃𝑖∃𝑗(𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ∃𝑖∃𝑗((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉))) |
30 | | r2ex 3222 |
. . . . . . . . . . . 12
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = 〈∅,
〈𝑖, 𝑗〉〉 ↔ ∃𝑖∃𝑗((𝑖 ∈ ω ∧ 𝑗 ∈ ω) ∧ 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉)) |
31 | 29, 30 | syl6ibr 255 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈∅, 𝑧〉 → (∃𝑖∃𝑗(𝑧 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉)) |
32 | 20, 31 | syl5com 31 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (ω ×
ω) → (𝑥 =
〈∅, 𝑧〉
→ ∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = 〈∅,
〈𝑖, 𝑗〉〉)) |
33 | 32 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑦 ∈ {∅} ∧ 𝑧 ∈ (ω ×
ω)) → (𝑥 =
〈∅, 𝑧〉
→ ∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = 〈∅,
〈𝑖, 𝑗〉〉)) |
34 | 19, 33 | sylbid 243 |
. . . . . . . 8
⊢ ((𝑦 ∈ {∅} ∧ 𝑧 ∈ (ω ×
ω)) → (𝑥 =
〈𝑦, 𝑧〉 → ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉)) |
35 | 34 | impcom 411 |
. . . . . . 7
⊢ ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ {∅} ∧ 𝑧 ∈ (ω × ω))) →
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = 〈∅,
〈𝑖, 𝑗〉〉) |
36 | 35 | exlimivv 1940 |
. . . . . 6
⊢
(∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ {∅} ∧ 𝑧 ∈ (ω × ω))) →
∃𝑖 ∈ ω
∃𝑗 ∈ ω
𝑥 = 〈∅,
〈𝑖, 𝑗〉〉) |
37 | 15, 36 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ ({∅} ×
(ω × ω)) → ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = 〈∅, 〈𝑖, 𝑗〉〉) |
38 | 14, 37 | impbii 212 |
. . . 4
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = 〈∅,
〈𝑖, 𝑗〉〉 ↔ 𝑥 ∈ ({∅} × (ω ×
ω))) |
39 | 6, 38 | bitri 278 |
. . 3
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω 𝑥 = (𝑖∈𝑔𝑗) ↔ 𝑥 ∈ ({∅} × (ω ×
ω))) |
40 | 3, 39 | mpgbir 1807 |
. 2
⊢ {𝑥 ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)} = ({∅} × (ω ×
ω)) |
41 | 1, 2, 40 | 3eqtri 2769 |
1
⊢
(Fmla‘∅) = ({∅} × (ω ×
ω)) |