Proof of Theorem setsstruct
Step | Hyp | Ref
| Expression |
1 | | simpr11 1138 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → 𝑀 ∈ ℕ) |
2 | | simpr12 1139 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → 𝑁 ∈ ℕ) |
3 | | eluznn 11634 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℕ ∧ 𝐼 ∈
(ℤ≥‘𝑀)) → 𝐼 ∈ ℕ) |
4 | 3 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → (𝐼 ∈
(ℤ≥‘𝑀) → 𝐼 ∈ ℕ)) |
5 | 4 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) → (𝐼 ∈ (ℤ≥‘𝑀) → 𝐼 ∈ ℕ)) |
6 | 5 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → (𝐼 ∈ (ℤ≥‘𝑀) → 𝐼 ∈ ℕ)) |
7 | 6 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ∈
(ℤ≥‘𝑀) → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → 𝐼 ∈ ℕ)) |
8 | 7 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → 𝐼 ∈ ℕ)) |
9 | 8 | imp 444 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → 𝐼 ∈ ℕ) |
10 | 2, 9 | ifcld 4081 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℕ) |
11 | | nnre 10904 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
12 | 11 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ ℝ) |
13 | | eluzelre 11574 |
. . . . . . . . . . . . 13
⊢ (𝐼 ∈
(ℤ≥‘𝑀) → 𝐼 ∈ ℝ) |
14 | 12, 13 | anim12i 588 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
15 | | nnre 10904 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
16 | 15 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℝ) |
17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ ℝ) |
18 | | simpl3 1059 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝑀 ≤ 𝑁) |
19 | 14, 17, 18 | 3jca 1235 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → ((𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ) ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≤ 𝑁)) |
20 | 19 | ex 449 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) → (𝐼 ∈ (ℤ≥‘𝑀) → ((𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ) ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≤ 𝑁))) |
21 | 20 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → (𝐼 ∈ (ℤ≥‘𝑀) → ((𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ) ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≤ 𝑁))) |
22 | 21 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ∈
(ℤ≥‘𝑀) → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → ((𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ) ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≤ 𝑁))) |
23 | 22 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → ((𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ) ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≤ 𝑁))) |
24 | 23 | imp 444 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → ((𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ) ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≤ 𝑁)) |
25 | | lemaxle 11900 |
. . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ 𝐼 ∈ ℝ) ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → 𝑀 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) |
27 | 1, 10, 26 | 3jca 1235 |
. . . 4
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → (𝑀 ∈ ℕ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℕ ∧ 𝑀 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
28 | | simp1 1054 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → 𝐺 ∈ 𝑈) |
29 | | simp2 1055 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → Fun (𝐺 ∖ {∅})) |
30 | 28, 29 | anim12i 588 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → (𝐺 ∈ 𝑈 ∧ Fun (𝐺 ∖ {∅}))) |
31 | | pm3.22 464 |
. . . . . . 7
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝐸 ∈ 𝑉)) |
32 | 31 | 3adant1 1072 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝐸 ∈ 𝑉)) |
33 | 32 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → (𝐼 ∈ (ℤ≥‘𝑀) ∧ 𝐸 ∈ 𝑉)) |
34 | | setsfun0 15726 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈
(ℤ≥‘𝑀) ∧ 𝐸 ∈ 𝑉)) → Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅})) |
35 | 30, 33, 34 | syl2anc 691 |
. . . 4
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅})) |
36 | | 3simpa 1051 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉)) |
37 | 36 | adantr 480 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → (𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉)) |
38 | | setsdm 15724 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉) → dom (𝐺 sSet 〈𝐼, 𝐸〉) = (dom 𝐺 ∪ {𝐼})) |
39 | 37, 38 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → dom (𝐺 sSet 〈𝐼, 𝐸〉) = (dom 𝐺 ∪ {𝐼})) |
40 | | simp3 1056 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → dom 𝐺 ⊆ (𝑀...𝑁)) |
41 | | nnz 11276 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
42 | 41 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ ℤ) |
43 | 42 | 3ad2ant1 1075 |
. . . . . 6
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → 𝑁 ∈ ℤ) |
44 | | simpl3 1059 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → 𝐼 ∈ (ℤ≥‘𝑀)) |
45 | | ssfzunsn 12257 |
. . . . . 6
⊢ ((dom
𝐺 ⊆ (𝑀...𝑁) ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (dom 𝐺 ∪ {𝐼}) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
46 | 40, 43, 44, 45 | syl2an23an 1379 |
. . . . 5
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → (dom 𝐺 ∪ {𝐼}) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
47 | 39, 46 | eqsstrd 3602 |
. . . 4
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → dom (𝐺 sSet 〈𝐼, 𝐸〉) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))) |
48 | 27, 35, 47 | 3jca 1235 |
. . 3
⊢ (((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) ∧ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) → ((𝑀 ∈ ℕ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℕ ∧ 𝑀 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) ∧ Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) ∧ dom (𝐺 sSet 〈𝐼, 𝐸〉) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))) |
49 | 48 | ex 449 |
. 2
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁)) → ((𝑀 ∈ ℕ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℕ ∧ 𝑀 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) ∧ Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) ∧ dom (𝐺 sSet 〈𝐼, 𝐸〉) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼))))) |
50 | | isstruct 15705 |
. 2
⊢ (𝐺 Struct 〈𝑀, 𝑁〉 ↔ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (𝑀...𝑁))) |
51 | | isstruct 15705 |
. 2
⊢ ((𝐺 sSet 〈𝐼, 𝐸〉) Struct 〈𝑀, if(𝐼 ≤ 𝑁, 𝑁, 𝐼)〉 ↔ ((𝑀 ∈ ℕ ∧ if(𝐼 ≤ 𝑁, 𝑁, 𝐼) ∈ ℕ ∧ 𝑀 ≤ if(𝐼 ≤ 𝑁, 𝑁, 𝐼)) ∧ Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) ∧ dom (𝐺 sSet 〈𝐼, 𝐸〉) ⊆ (𝑀...if(𝐼 ≤ 𝑁, 𝑁, 𝐼)))) |
52 | 49, 50, 51 | 3imtr4g 284 |
1
⊢ ((𝐺 ∈ 𝑈 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ (ℤ≥‘𝑀)) → (𝐺 Struct 〈𝑀, 𝑁〉 → (𝐺 sSet 〈𝐼, 𝐸〉) Struct 〈𝑀, if(𝐼 ≤ 𝑁, 𝑁, 𝐼)〉)) |