Step | Hyp | Ref
| Expression |
1 | | simpll 497 |
. 2
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ))) |
2 | | simplr 498 |
. 2
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → Fun (𝐹 ∖ {∅})) |
3 | | simprr 500 |
. 2
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → dom 𝐹 ⊆ (...‘𝑋)) |
4 | | simprl 499 |
. . . 4
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝐹 ∈ 𝑉) |
5 | 4 | elexd 2646 |
. . 3
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝐹 ∈ V) |
6 | | elex 2644 |
. . . 4
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
∈ V) |
7 | 6 | ad2antrr 473 |
. . 3
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝑋 ∈ V) |
8 | | simpr 109 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
9 | 8 | eleq1d 2163 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ↔ 𝑋 ∈ (
≤ ∩ (ℕ × ℕ)))) |
10 | | simpl 108 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → 𝑓 = 𝐹) |
11 | 10 | difeq1d 3132 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (𝑓 ∖ {∅}) = (𝐹 ∖ {∅})) |
12 | 11 | funeqd 5071 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (Fun (𝑓 ∖ {∅}) ↔ Fun (𝐹 ∖
{∅}))) |
13 | 10 | dmeqd 4669 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → dom 𝑓 = dom 𝐹) |
14 | 8 | fveq2d 5344 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (...‘𝑥) = (...‘𝑋)) |
15 | 13, 14 | sseq12d 3070 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (dom 𝑓 ⊆ (...‘𝑥) ↔ dom 𝐹 ⊆ (...‘𝑋))) |
16 | 9, 12, 15 | 3anbi123d 1255 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → ((𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝑓
∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥)) ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
17 | | df-struct 11660 |
. . . 4
⊢ Struct =
{〈𝑓, 𝑥〉 ∣ (𝑥 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} |
18 | 16, 17 | brabga 4115 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝑋 ∈ V) → (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
19 | 5, 7, 18 | syl2anc 404 |
. 2
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
20 | 1, 2, 3, 19 | mpbir3and 1129 |
1
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝐹 Struct 𝑋) |