Step | Hyp | Ref
| Expression |
1 | | isstruct2 16492 |
. . . . . . 7
⊢ (𝐺 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐺
∖ {∅}) ∧ dom 𝐺 ⊆ (...‘𝑋))) |
2 | | elin 3897 |
. . . . . . . . 9
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ↔ (𝑋
∈ ≤ ∧ 𝑋 ∈
(ℕ × ℕ))) |
3 | | elxp6 7712 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (ℕ ×
ℕ) ↔ (𝑋 =
⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∧ ((1^{st} ‘𝑋) ∈ ℕ ∧
(2^{nd} ‘𝑋)
∈ ℕ))) |
4 | | eleq1 2877 |
. . . . . . . . . . . . 13
⊢ (𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ →
(𝑋 ∈ ≤ ↔
⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ )) |
5 | 4 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (𝑋 ∈ ≤ ↔ ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∈ ≤
)) |
6 | | simp3 1135 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → 𝐼 ∈ ℕ) |
7 | | simp1l 1194 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → (1^{st}
‘𝑋) ∈
ℕ) |
8 | 6, 7 | ifcld 4470 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)) ∈ ℕ) |
9 | 8 | nnred 11647 |
. . . . . . . . . . . . . . . . 17
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)) ∈ ℝ) |
10 | 6 | nnred 11647 |
. . . . . . . . . . . . . . . . 17
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → 𝐼 ∈ ℝ) |
11 | | simp1r 1195 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → (2^{nd}
‘𝑋) ∈
ℕ) |
12 | 11, 6 | ifcld 4470 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼) ∈ ℕ) |
13 | 12 | nnred 11647 |
. . . . . . . . . . . . . . . . 17
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼) ∈ ℝ) |
14 | | nnre 11639 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1^{st} ‘𝑋) ∈ ℕ → (1^{st}
‘𝑋) ∈
ℝ) |
15 | 14 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
→ (1^{st} ‘𝑋) ∈ ℝ) |
16 | | nnre 11639 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ ℕ → 𝐼 ∈
ℝ) |
17 | 15, 16 | anim12i 615 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ 𝐼 ∈ ℕ)
→ ((1^{st} ‘𝑋) ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
18 | 17 | 3adant2 1128 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ((1^{st}
‘𝑋) ∈ ℝ
∧ 𝐼 ∈
ℝ)) |
19 | 18 | ancomd 465 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → (𝐼 ∈ ℝ ∧ (1^{st}
‘𝑋) ∈
ℝ)) |
20 | | min1 12577 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ ℝ ∧
(1^{st} ‘𝑋)
∈ ℝ) → if(𝐼
≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)) ≤ 𝐼) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)) ≤ 𝐼) |
22 | | nnre 11639 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑋) ∈ ℕ → (2^{nd}
‘𝑋) ∈
ℝ) |
23 | 22 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
→ (2^{nd} ‘𝑋) ∈ ℝ) |
24 | 23, 16 | anim12i 615 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ 𝐼 ∈ ℕ)
→ ((2^{nd} ‘𝑋) ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
25 | 24 | 3adant2 1128 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ((2^{nd}
‘𝑋) ∈ ℝ
∧ 𝐼 ∈
ℝ)) |
26 | 25 | ancomd 465 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → (𝐼 ∈ ℝ ∧ (2^{nd}
‘𝑋) ∈
ℝ)) |
27 | | max1 12573 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ ℝ ∧
(2^{nd} ‘𝑋)
∈ ℝ) → 𝐼
≤ if(𝐼 ≤
(2^{nd} ‘𝑋),
(2^{nd} ‘𝑋),
𝐼)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → 𝐼 ≤ if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)) |
29 | 9, 10, 13, 21, 28 | letrd 10793 |
. . . . . . . . . . . . . . . 16
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)) ≤ if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)) |
30 | | df-br 5032 |
. . . . . . . . . . . . . . . 16
⊢ (if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)) ≤ if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼) ↔ ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ≤ ) |
31 | 29, 30 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ≤ ) |
32 | 8, 12 | opelxpd 5558 |
. . . . . . . . . . . . . . 15
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ (ℕ ×
ℕ)) |
33 | 31, 32 | elind 4121 |
. . . . . . . . . . . . . 14
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))) |
34 | 33 | 3exp 1116 |
. . . . . . . . . . . . 13
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
→ (⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ → (𝐼 ∈ ℕ →
⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩
(ℕ × ℕ))))) |
35 | 34 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) →
(⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ → (𝐼 ∈ ℕ →
⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩
(ℕ × ℕ))))) |
36 | 5, 35 | sylbid 243 |
. . . . . . . . . . 11
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (𝑋 ∈ ≤ → (𝐼 ∈ ℕ → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))))) |
37 | 3, 36 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (ℕ ×
ℕ) → (𝑋 ∈
≤ → (𝐼 ∈
ℕ → ⟨if(𝐼
≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))))) |
38 | 37 | impcom 411 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ≤ ∧ 𝑋 ∈ (ℕ ×
ℕ)) → (𝐼 ∈
ℕ → ⟨if(𝐼
≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)))) |
39 | 2, 38 | sylbi 220 |
. . . . . . . 8
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → (𝐼
∈ ℕ → ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)))) |
40 | 39 | 3ad2ant1 1130 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (...‘𝑋)) → (𝐼 ∈ ℕ → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)))) |
41 | 1, 40 | sylbi 220 |
. . . . . 6
⊢ (𝐺 Struct 𝑋 → (𝐼 ∈ ℕ → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)))) |
42 | 41 | imp 410 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))) |
43 | 42 | 3adant2 1128 |
. . . 4
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))) |
44 | | structex 16493 |
. . . . . . 7
⊢ (𝐺 Struct 𝑋 → 𝐺 ∈ V) |
45 | | structn0fun 16494 |
. . . . . . 7
⊢ (𝐺 Struct 𝑋 → Fun (𝐺 ∖ {∅})) |
46 | 44, 45 | jca 515 |
. . . . . 6
⊢ (𝐺 Struct 𝑋 → (𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅}))) |
47 | 46 | 3ad2ant1 1130 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → (𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅}))) |
48 | | simp3 1135 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → 𝐼 ∈ ℕ) |
49 | | simp2 1134 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → 𝐸 ∈ 𝑉) |
50 | | setsfun0 16518 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅})) ∧
(𝐼 ∈ ℕ ∧
𝐸 ∈ 𝑉)) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅})) |
51 | 47, 48, 49, 50 | syl12anc 835 |
. . . 4
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅})) |
52 | 44 | 3ad2ant1 1130 |
. . . . . 6
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → 𝐺 ∈ V) |
53 | | setsdm 16516 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐸 ∈ 𝑉) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) = (dom 𝐺 ∪ {𝐼})) |
54 | 52, 49, 53 | syl2anc 587 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) = (dom 𝐺 ∪ {𝐼})) |
55 | | fveq2 6650 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ →
(...‘𝑋) =
(...‘⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩)) |
56 | | df-ov 7143 |
. . . . . . . . . . . . . . . . 17
⊢
((1^{st} ‘𝑋)...(2^{nd} ‘𝑋)) = (...‘⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩) |
57 | 55, 56 | eqtr4di 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ →
(...‘𝑋) =
((1^{st} ‘𝑋)...(2^{nd} ‘𝑋))) |
58 | 57 | sseq2d 3947 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ → (dom
𝐺 ⊆ (...‘𝑋) ↔ dom 𝐺 ⊆ ((1^{st} ‘𝑋)...(2^{nd} ‘𝑋)))) |
59 | 58 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (dom 𝐺 ⊆ (...‘𝑋) ↔ dom 𝐺 ⊆ ((1^{st} ‘𝑋)...(2^{nd} ‘𝑋)))) |
60 | | df-3an 1086 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ
∧ 𝐼 ∈ ℕ)
↔ (((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ 𝐼 ∈
ℕ)) |
61 | | nnz 11999 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1^{st} ‘𝑋) ∈ ℕ → (1^{st}
‘𝑋) ∈
ℤ) |
62 | | nnz 11999 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑋) ∈ ℕ → (2^{nd}
‘𝑋) ∈
ℤ) |
63 | | nnz 11999 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ ℕ → 𝐼 ∈
ℤ) |
64 | 61, 62, 63 | 3anim123i 1148 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ
∧ 𝐼 ∈ ℕ)
→ ((1^{st} ‘𝑋) ∈ ℤ ∧ (2^{nd}
‘𝑋) ∈ ℤ
∧ 𝐼 ∈
ℤ)) |
65 | | ssfzunsnext 12954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) ∧
((1^{st} ‘𝑋)
∈ ℤ ∧ (2^{nd} ‘𝑋) ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (dom 𝐺 ∪ {𝐼}) ⊆ (if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋))...if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼))) |
66 | | df-ov 7143 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋))...if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)) = (...‘⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) |
67 | 65, 66 | sseqtrdi 3965 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) ∧
((1^{st} ‘𝑋)
∈ ℤ ∧ (2^{nd} ‘𝑋) ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
68 | 64, 67 | sylan2 595 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ ∧ 𝐼 ∈ ℕ)) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
69 | 68 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) →
(((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ ∧ 𝐼 ∈ ℕ) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
70 | 60, 69 | syl5bir 246 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) →
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ 𝐼 ∈ ℕ)
→ (dom 𝐺 ∪ {𝐼}) ⊆
(...‘⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩))) |
71 | 70 | expd 419 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) →
(((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
72 | 71 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
→ (dom 𝐺 ⊆
((1^{st} ‘𝑋)...(2^{nd} ‘𝑋)) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
73 | 72 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (dom 𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) → (𝐼 ∈ ℕ → (dom
𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
74 | 59, 73 | sylbid 243 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (dom 𝐺 ⊆ (...‘𝑋) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
75 | 3, 74 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (ℕ ×
ℕ) → (dom 𝐺
⊆ (...‘𝑋)
→ (𝐼 ∈ ℕ
→ (dom 𝐺 ∪ {𝐼}) ⊆
(...‘⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩)))) |
76 | 75 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ≤ ∧ 𝑋 ∈ (ℕ ×
ℕ)) → (dom 𝐺
⊆ (...‘𝑋)
→ (𝐼 ∈ ℕ
→ (dom 𝐺 ∪ {𝐼}) ⊆
(...‘⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩)))) |
77 | 2, 76 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → (dom 𝐺 ⊆ (...‘𝑋) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
78 | 77 | imp 410 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ dom 𝐺 ⊆ (...‘𝑋)) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
79 | 78 | 3adant2 1128 |
. . . . . . . 8
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (...‘𝑋)) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
80 | 1, 79 | sylbi 220 |
. . . . . . 7
⊢ (𝐺 Struct 𝑋 → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
81 | 80 | imp 410 |
. . . . . 6
⊢ ((𝐺 Struct 𝑋 ∧ 𝐼 ∈ ℕ) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
82 | 81 | 3adant2 1128 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
83 | 54, 82 | eqsstrd 3953 |
. . . 4
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
84 | | isstruct2 16492 |
. . . 4
⊢ ((𝐺 sSet ⟨𝐼, 𝐸⟩) Struct ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ↔ (⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun ((𝐺
sSet ⟨𝐼, 𝐸⟩) ∖ {∅}) ∧
dom (𝐺 sSet ⟨𝐼, 𝐸⟩) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
85 | 43, 51, 83, 84 | syl3anbrc 1340 |
. . 3
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) |
86 | 85 | adantr 484 |
. 2
⊢ (((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) ∧ 𝑌 = ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) → (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) |
87 | | breq2 5035 |
. . 3
⊢ (𝑌 = ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ → ((𝐺 sSet ⟨𝐼, 𝐸⟩) Struct 𝑌 ↔ (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
88 | 87 | adantl 485 |
. 2
⊢ (((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) ∧ 𝑌 = ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) → ((𝐺 sSet ⟨𝐼, 𝐸⟩) Struct 𝑌 ↔ (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
89 | 86, 88 | mpbird 260 |
1
⊢ (((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) ∧ 𝑌 = ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) → (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct 𝑌) |