Step | Hyp | Ref
| Expression |
1 | | brstruct 15703 |
. . 3
⊢ Rel
Struct |
2 | | brrelex12 5079 |
. . 3
⊢ ((Rel
Struct ∧ 𝐹 Struct 𝑋) → (𝐹 ∈ V ∧ 𝑋 ∈ V)) |
3 | 1, 2 | mpan 702 |
. 2
⊢ (𝐹 Struct 𝑋 → (𝐹 ∈ V ∧ 𝑋 ∈ V)) |
4 | | ssun1 3738 |
. . . . 5
⊢ 𝐹 ⊆ (𝐹 ∪ {∅}) |
5 | | undif1 3995 |
. . . . 5
⊢ ((𝐹 ∖ {∅}) ∪
{∅}) = (𝐹 ∪
{∅}) |
6 | 4, 5 | sseqtr4i 3601 |
. . . 4
⊢ 𝐹 ⊆ ((𝐹 ∖ {∅}) ∪
{∅}) |
7 | | simp2 1055 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → Fun (𝐹 ∖ {∅})) |
8 | | funfn 5833 |
. . . . . . 7
⊢ (Fun
(𝐹 ∖ {∅})
↔ (𝐹 ∖
{∅}) Fn dom (𝐹
∖ {∅})) |
9 | 7, 8 | sylib 207 |
. . . . . 6
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∖ {∅}) Fn dom (𝐹 ∖
{∅})) |
10 | | inss2 3796 |
. . . . . . . . . . . 12
⊢ ( ≤
∩ (ℕ × ℕ)) ⊆ (ℕ ×
ℕ) |
11 | 10 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
∈ (ℕ × ℕ)) |
12 | | 1st2nd2 7096 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (ℕ ×
ℕ) → 𝑋 =
〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
= 〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
14 | 13 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝑋 = 〈(1st ‘𝑋), (2nd ‘𝑋)〉) |
15 | 14 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (...‘𝑋) =
(...‘〈(1st ‘𝑋), (2nd ‘𝑋)〉)) |
16 | | df-ov 6552 |
. . . . . . . . 9
⊢
((1st ‘𝑋)...(2nd ‘𝑋)) = (...‘〈(1st
‘𝑋), (2nd
‘𝑋)〉) |
17 | | fzfi 12633 |
. . . . . . . . 9
⊢
((1st ‘𝑋)...(2nd ‘𝑋)) ∈ Fin |
18 | 16, 17 | eqeltrri 2685 |
. . . . . . . 8
⊢
(...‘〈(1st ‘𝑋), (2nd ‘𝑋)〉) ∈ Fin |
19 | 15, 18 | syl6eqel 2696 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (...‘𝑋) ∈ Fin) |
20 | | difss 3699 |
. . . . . . . . 9
⊢ (𝐹 ∖ {∅}) ⊆
𝐹 |
21 | | dmss 5245 |
. . . . . . . . 9
⊢ ((𝐹 ∖ {∅}) ⊆
𝐹 → dom (𝐹 ∖ {∅}) ⊆ dom
𝐹) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
⊢ dom
(𝐹 ∖ {∅})
⊆ dom 𝐹 |
23 | | simp3 1056 |
. . . . . . . 8
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom 𝐹 ⊆ (...‘𝑋)) |
24 | 22, 23 | syl5ss 3579 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom (𝐹 ∖ {∅}) ⊆ (...‘𝑋)) |
25 | | ssfi 8065 |
. . . . . . 7
⊢
(((...‘𝑋)
∈ Fin ∧ dom (𝐹
∖ {∅}) ⊆ (...‘𝑋)) → dom (𝐹 ∖ {∅}) ∈
Fin) |
26 | 19, 24, 25 | syl2anc 691 |
. . . . . 6
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → dom (𝐹 ∖ {∅}) ∈
Fin) |
27 | | fnfi 8123 |
. . . . . 6
⊢ (((𝐹 ∖ {∅}) Fn dom
(𝐹 ∖ {∅}) ∧
dom (𝐹 ∖ {∅})
∈ Fin) → (𝐹
∖ {∅}) ∈ Fin) |
28 | 9, 26, 27 | syl2anc 691 |
. . . . 5
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∖ {∅}) ∈
Fin) |
29 | | p0ex 4779 |
. . . . 5
⊢ {∅}
∈ V |
30 | | unexg 6857 |
. . . . 5
⊢ (((𝐹 ∖ {∅}) ∈ Fin
∧ {∅} ∈ V) → ((𝐹 ∖ {∅}) ∪ {∅}) ∈
V) |
31 | 28, 29, 30 | sylancl 693 |
. . . 4
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → ((𝐹 ∖ {∅}) ∪ {∅}) ∈
V) |
32 | | ssexg 4732 |
. . . 4
⊢ ((𝐹 ⊆ ((𝐹 ∖ {∅}) ∪ {∅}) ∧
((𝐹 ∖ {∅})
∪ {∅}) ∈ V) → 𝐹 ∈ V) |
33 | 6, 31, 32 | sylancr 694 |
. . 3
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝐹 ∈ V) |
34 | | elex 3185 |
. . . 4
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → 𝑋
∈ V) |
35 | 34 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → 𝑋 ∈ V) |
36 | 33, 35 | jca 553 |
. 2
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)) → (𝐹 ∈ V ∧ 𝑋 ∈ V)) |
37 | | simpr 476 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
38 | 37 | eleq1d 2672 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ↔ 𝑋 ∈ (
≤ ∩ (ℕ × ℕ)))) |
39 | | simpl 472 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → 𝑓 = 𝐹) |
40 | 39 | difeq1d 3689 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (𝑓 ∖ {∅}) = (𝐹 ∖ {∅})) |
41 | 40 | funeqd 5825 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (Fun (𝑓 ∖ {∅}) ↔ Fun (𝐹 ∖
{∅}))) |
42 | 39 | dmeqd 5248 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → dom 𝑓 = dom 𝐹) |
43 | 37 | fveq2d 6107 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (...‘𝑥) = (...‘𝑋)) |
44 | 42, 43 | sseq12d 3597 |
. . . 4
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → (dom 𝑓 ⊆ (...‘𝑥) ↔ dom 𝐹 ⊆ (...‘𝑋))) |
45 | 38, 41, 44 | 3anbi123d 1391 |
. . 3
⊢ ((𝑓 = 𝐹 ∧ 𝑥 = 𝑋) → ((𝑥 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝑓
∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥)) ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
46 | | df-struct 15697 |
. . 3
⊢ Struct =
{〈𝑓, 𝑥〉 ∣ (𝑥 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} |
47 | 45, 46 | brabga 4914 |
. 2
⊢ ((𝐹 ∈ V ∧ 𝑋 ∈ V) → (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋)))) |
48 | 3, 36, 47 | pm5.21nii 367 |
1
⊢ (𝐹 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐹
∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋))) |