Step | Hyp | Ref
| Expression |
1 | | brstruct 16535 |
. . 3
⊢ Rel
Struct |
2 | 1 | brrelex12i 5569 |
. 2
⊢ (𝐹 Struct 𝑋 → (𝐹 ∈ V ∧ 𝑋 ∈ V)) |
3 | | ssun1 4073 |
. . . . 5
⊢ 𝐹 ⊆ (𝐹 ∪ {∅}) |
4 | | undif1 4365 |
. . . . 5
⊢ ((𝐹 ∖ {∅}) ∪
{∅}) = (𝐹 ∪
{∅}) |
5 | 3, 4 | sseqtrri 3925 |
. . . 4
⊢ 𝐹 ⊆ ((𝐹 ∖ {∅}) ∪
{∅}) |
6 | | simp2 1135 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → Fun (𝐹 ∖ {∅})) |
7 | 6 | funfnd 6359 |
. . . . . 6
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∖ {∅}) Fn dom (𝐹 ∖
{∅})) |
8 | | elinel2 4097 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
∈ (ℕ × ℕ)) |
9 | | 1st2nd2 7725 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (ℕ ×
ℕ) → 𝑋 =
〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
= 〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
11 | 10 | 3ad2ant1 1131 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝑋 = 〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
12 | 11 | fveq2d 6655 |
. . . . . . . 8
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (...‘𝑋) =
(...‘〈(1st ‘𝑋), (2nd ‘𝑋)〉)) |
13 | | df-ov 7146 |
. . . . . . . . 9
⊢
((1st ‘𝑋)...(2nd ‘𝑋)) = (...‘〈(1st
‘𝑋), (2nd
‘𝑋)〉) |
14 | | fzfi 13374 |
. . . . . . . . 9
⊢
((1st ‘𝑋)...(2nd ‘𝑋)) ∈ Fin |
15 | 13, 14 | eqeltrri 2848 |
. . . . . . . 8
⊢
(...‘〈(1st ‘𝑋), (2nd ‘𝑋)〉) ∈ Fin |
16 | 12, 15 | eqeltrdi 2859 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (...‘𝑋) ∈ Fin) |
17 | | difss 4033 |
. . . . . . . . 9
⊢ (𝐹 ∖ {∅}) ⊆
𝐹 |
18 | | dmss 5735 |
. . . . . . . . 9
⊢ ((𝐹 ∖ {∅}) ⊆
𝐹 → dom (𝐹 ∖ {∅}) ⊆ dom
𝐹) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝐹 ∖ {∅})
⊆ dom 𝐹 |
20 | | simp3 1136 |
. . . . . . . 8
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom 𝐹 ⊆ (...‘𝑋)) |
21 | 19, 20 | sstrid 3899 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom (𝐹 ∖ {∅}) ⊆ (...‘𝑋)) |
22 | 16, 21 | ssfid 8755 |
. . . . . 6
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom (𝐹 ∖ {∅}) ∈
Fin) |
23 | | fnfi 8814 |
. . . . . 6
⊢ (((𝐹 ∖ {∅}) Fn dom
(𝐹 ∖ {∅}) ∧
dom (𝐹 ∖ {∅})
∈ Fin) → (𝐹
∖ {∅}) ∈ Fin) |
24 | 7, 22, 23 | syl2anc 588 |
. . . . 5
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∖ {∅}) ∈
Fin) |
25 | | p0ex 5246 |
. . . . 5
⊢ {∅}
∈ V |
26 | | unexg 7463 |
. . . . 5
⊢ (((𝐹 ∖ {∅}) ∈ Fin
∧ {∅} ∈ V) → ((𝐹 ∖ {∅}) ∪ {∅}) ∈
V) |
27 | 24, 25, 26 | sylancl 590 |
. . . 4
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → ((𝐹 ∖ {∅}) ∪ {∅}) ∈
V) |
28 | | ssexg 5186 |
. . . 4
⊢ ((𝐹 ⊆ ((𝐹 ∖ {∅}) ∪ {∅}) ∧
((𝐹 ∖ {∅})
∪ {∅}) ∈ V) → 𝐹 ∈ V) |
29 | 5, 27, 28 | sylancr 591 |
. . 3
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝐹 ∈ V) |
30 | | elex 3427 |
. . . 4
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
∈ V) |
31 | 30 | 3ad2ant1 1131 |
. . 3
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝑋 ∈ V) |
32 | 29, 31 | jca 516 |
. 2
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∈ V ∧ 𝑋 ∈ V)) |
33 | | simpr 489 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
34 | 33 | eleq1d 2835 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ↔ 𝑋 ∈ (
≤ ∩ (ℕ × ℕ)))) |
35 | | simpl 487 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → 𝑓 = 𝐹) |
36 | 35 | difeq1d 4023 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (𝑓 ∖ {∅}) = (𝐹 ∖ {∅})) |
37 | 36 | funeqd 6350 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (Fun (𝑓 ∖ {∅}) ↔ Fun (𝐹 ∖
{∅}))) |
38 | 35 | dmeqd 5738 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → dom 𝑓 = dom 𝐹) |
39 | 33 | fveq2d 6655 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (...‘𝑥) = (...‘𝑋)) |
40 | 38, 39 | sseq12d 3921 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (dom 𝑓 ⊆ (...‘𝑥) ↔ dom 𝐹 ⊆ (...‘𝑋))) |
41 | 34, 37, 40 | 3anbi123d 1434 |
. . 3
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → ((𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝑓
∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥)) ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
42 | | df-struct 16528 |
. . 3
⊢ Struct =
{〈𝑓, 𝑥〉 ∣ (𝑥 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} |
43 | 41, 42 | brabga 5384 |
. 2
⊢ ((𝐹 ∈ V ∧ 𝑋 ∈ V) → (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
44 | 2, 32, 43 | pm5.21nii 384 |
1
⊢ (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋))) |