Step | Hyp | Ref
| Expression |
1 | | brstruct 17081 |
. . 3
⊢ Rel
Struct |
2 | 1 | brrelex12i 5732 |
. 2
⊢ (𝐹 Struct 𝑋 → (𝐹 ∈ V ∧ 𝑋 ∈ V)) |
3 | | ssun1 4173 |
. . . . 5
⊢ 𝐹 ⊆ (𝐹 ∪ {∅}) |
4 | | undif1 4476 |
. . . . 5
⊢ ((𝐹 ∖ {∅}) ∪
{∅}) = (𝐹 ∪
{∅}) |
5 | 3, 4 | sseqtrri 4020 |
. . . 4
⊢ 𝐹 ⊆ ((𝐹 ∖ {∅}) ∪
{∅}) |
6 | | simp2 1138 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → Fun (𝐹 ∖ {∅})) |
7 | 6 | funfnd 6580 |
. . . . . 6
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∖ {∅}) Fn dom (𝐹 ∖
{∅})) |
8 | | elinel2 4197 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
∈ (ℕ × ℕ)) |
9 | | 1st2nd2 8014 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (ℕ ×
ℕ) → 𝑋 =
⟨(1st ‘𝑋), (2nd ‘𝑋)⟩) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
= ⟨(1st ‘𝑋), (2nd ‘𝑋)⟩) |
11 | 10 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝑋 = ⟨(1st ‘𝑋), (2nd ‘𝑋)⟩) |
12 | 11 | fveq2d 6896 |
. . . . . . . 8
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (...‘𝑋) =
(...‘⟨(1st ‘𝑋), (2nd ‘𝑋)⟩)) |
13 | | df-ov 7412 |
. . . . . . . . 9
⊢
((1st ‘𝑋)...(2nd ‘𝑋)) = (...‘⟨(1st
‘𝑋), (2nd
‘𝑋)⟩) |
14 | | fzfi 13937 |
. . . . . . . . 9
⊢
((1st ‘𝑋)...(2nd ‘𝑋)) ∈ Fin |
15 | 13, 14 | eqeltrri 2831 |
. . . . . . . 8
⊢
(...‘⟨(1st ‘𝑋), (2nd ‘𝑋)⟩) ∈ Fin |
16 | 12, 15 | eqeltrdi 2842 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (...‘𝑋) ∈ Fin) |
17 | | difss 4132 |
. . . . . . . . 9
⊢ (𝐹 ∖ {∅}) ⊆
𝐹 |
18 | | dmss 5903 |
. . . . . . . . 9
⊢ ((𝐹 ∖ {∅}) ⊆
𝐹 → dom (𝐹 ∖ {∅}) ⊆ dom
𝐹) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝐹 ∖ {∅})
⊆ dom 𝐹 |
20 | | simp3 1139 |
. . . . . . . 8
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom 𝐹 ⊆ (...‘𝑋)) |
21 | 19, 20 | sstrid 3994 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom (𝐹 ∖ {∅}) ⊆ (...‘𝑋)) |
22 | 16, 21 | ssfid 9267 |
. . . . . 6
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom (𝐹 ∖ {∅}) ∈
Fin) |
23 | | fnfi 9181 |
. . . . . 6
⊢ (((𝐹 ∖ {∅}) Fn dom
(𝐹 ∖ {∅}) ∧
dom (𝐹 ∖ {∅})
∈ Fin) → (𝐹
∖ {∅}) ∈ Fin) |
24 | 7, 22, 23 | syl2anc 585 |
. . . . 5
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∖ {∅}) ∈
Fin) |
25 | | p0ex 5383 |
. . . . 5
⊢ {∅}
∈ V |
26 | | unexg 7736 |
. . . . 5
⊢ (((𝐹 ∖ {∅}) ∈ Fin
∧ {∅} ∈ V) → ((𝐹 ∖ {∅}) ∪ {∅}) ∈
V) |
27 | 24, 25, 26 | sylancl 587 |
. . . 4
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → ((𝐹 ∖ {∅}) ∪ {∅}) ∈
V) |
28 | | ssexg 5324 |
. . . 4
⊢ ((𝐹 ⊆ ((𝐹 ∖ {∅}) ∪ {∅}) ∧
((𝐹 ∖ {∅})
∪ {∅}) ∈ V) → 𝐹 ∈ V) |
29 | 5, 27, 28 | sylancr 588 |
. . 3
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝐹 ∈ V) |
30 | | elex 3493 |
. . . 4
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
∈ V) |
31 | 30 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝑋 ∈ V) |
32 | 29, 31 | jca 513 |
. 2
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∈ V ∧ 𝑋 ∈ V)) |
33 | | simpr 486 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
34 | 33 | eleq1d 2819 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ↔ 𝑋 ∈ (
≤ ∩ (ℕ × ℕ)))) |
35 | | simpl 484 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → 𝑓 = 𝐹) |
36 | 35 | difeq1d 4122 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (𝑓 ∖ {∅}) = (𝐹 ∖ {∅})) |
37 | 36 | funeqd 6571 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (Fun (𝑓 ∖ {∅}) ↔ Fun (𝐹 ∖
{∅}))) |
38 | 35 | dmeqd 5906 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → dom 𝑓 = dom 𝐹) |
39 | 33 | fveq2d 6896 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (...‘𝑥) = (...‘𝑋)) |
40 | 38, 39 | sseq12d 4016 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (dom 𝑓 ⊆ (...‘𝑥) ↔ dom 𝐹 ⊆ (...‘𝑋))) |
41 | 34, 37, 40 | 3anbi123d 1437 |
. . 3
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → ((𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝑓
∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥)) ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
42 | | df-struct 17080 |
. . 3
⊢ Struct =
{⟨𝑓, 𝑥⟩ ∣ (𝑥 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} |
43 | 41, 42 | brabga 5535 |
. 2
⊢ ((𝐹 ∈ V ∧ 𝑋 ∈ V) → (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
44 | 2, 32, 43 | pm5.21nii 380 |
1
⊢ (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋))) |