Step | Hyp | Ref
| Expression |
1 | | isstruct2 16194 |
. . . . . . 7
⊢ (𝐺 Struct 𝑋 ↔ (𝑋 ∈ ( ≤ ∩ (ℕ ×
ℕ)) ∧ Fun (𝐺
∖ {∅}) ∧ dom 𝐺 ⊆ (...‘𝑋))) |
2 | | elin 3994 |
. . . . . . . . 9
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ↔ (𝑋
∈ ≤ ∧ 𝑋 ∈
(ℕ × ℕ))) |
3 | | elxp6 7435 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (ℕ ×
ℕ) ↔ (𝑋 =
⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∧ ((1^{st} ‘𝑋) ∈ ℕ ∧
(2^{nd} ‘𝑋)
∈ ℕ))) |
4 | | eleq1 2866 |
. . . . . . . . . . . . 13
⊢ (𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ →
(𝑋 ∈ ≤ ↔
⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ )) |
5 | 4 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (𝑋 ∈ ≤ ↔ ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∈ ≤
)) |
6 | | simp3 1169 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → 𝐼 ∈ ℕ) |
7 | | simp1l 1255 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → (1^{st}
‘𝑋) ∈
ℕ) |
8 | 6, 7 | ifcld 4322 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)) ∈ ℕ) |
9 | 8 | nnred 11329 |
. . . . . . . . . . . . . . . . 17
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)) ∈ ℝ) |
10 | 6 | nnred 11329 |
. . . . . . . . . . . . . . . . 17
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → 𝐼 ∈ ℝ) |
11 | | simp1r 1256 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → (2^{nd}
‘𝑋) ∈
ℕ) |
12 | 11, 6 | ifcld 4322 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼) ∈ ℕ) |
13 | 12 | nnred 11329 |
. . . . . . . . . . . . . . . . 17
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼) ∈ ℝ) |
14 | | nnre 11320 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((1^{st} ‘𝑋) ∈ ℕ → (1^{st}
‘𝑋) ∈
ℝ) |
15 | 14 | adantr 473 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
→ (1^{st} ‘𝑋) ∈ ℝ) |
16 | | nnre 11320 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ ℕ → 𝐼 ∈
ℝ) |
17 | 15, 16 | anim12i 607 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ 𝐼 ∈ ℕ)
→ ((1^{st} ‘𝑋) ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
18 | 17 | 3adant2 1162 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ((1^{st}
‘𝑋) ∈ ℝ
∧ 𝐼 ∈
ℝ)) |
19 | 18 | ancomd 454 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → (𝐼 ∈ ℝ ∧ (1^{st}
‘𝑋) ∈
ℝ)) |
20 | | min1 12269 |
. . . . . . . . . . . . . . . . . 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 11320 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2^{nd} ‘𝑋) ∈ ℕ → (2^{nd}
‘𝑋) ∈
ℝ) |
23 | 22 | adantl 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
→ (2^{nd} ‘𝑋) ∈ ℝ) |
24 | 23, 16 | anim12i 607 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ 𝐼 ∈ ℕ)
→ ((2^{nd} ‘𝑋) ∈ ℝ ∧ 𝐼 ∈ ℝ)) |
25 | 24 | 3adant2 1162 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ((2^{nd}
‘𝑋) ∈ ℝ
∧ 𝐼 ∈
ℝ)) |
26 | 25 | ancomd 454 |
. . . . . . . . . . . . . . . . . 18
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → (𝐼 ∈ ℝ ∧ (2^{nd}
‘𝑋) ∈
ℝ)) |
27 | | max1 12265 |
. . . . . . . . . . . . . . . . . 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 10484 |
. . . . . . . . . . . . . . . 16
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)) ≤ if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)) |
30 | | df-br 4844 |
. . . . . . . . . . . . . . . 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 210 |
. . . . . . . . . . . . . . 15
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ≤ ) |
32 | 8, 12 | opelxpd 5350 |
. . . . . . . . . . . . . . 15
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ (ℕ ×
ℕ)) |
33 | 31, 32 | elind 3996 |
. . . . . . . . . . . . . 14
⊢
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ ⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))) |
34 | 33 | 3exp 1149 |
. . . . . . . . . . . . 13
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
→ (⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩ ∈ ≤ → (𝐼 ∈ ℕ →
⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩
(ℕ × ℕ))))) |
35 | 34 | adantl 474 |
. . . . . . . . . . . 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 232 |
. . . . . . . . . . 11
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (𝑋 ∈ ≤ → (𝐼 ∈ ℕ → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))))) |
37 | 3, 36 | sylbi 209 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (ℕ ×
ℕ) → (𝑋 ∈
≤ → (𝐼 ∈
ℕ → ⟨if(𝐼
≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))))) |
38 | 37 | impcom 397 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ≤ ∧ 𝑋 ∈ (ℕ ×
ℕ)) → (𝐼 ∈
ℕ → ⟨if(𝐼
≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)))) |
39 | 2, 38 | sylbi 209 |
. . . . . . . 8
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → (𝐼
∈ ℕ → ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)))) |
40 | 39 | 3ad2ant1 1164 |
. . . . . . 7
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (...‘𝑋)) → (𝐼 ∈ ℕ → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)))) |
41 | 1, 40 | sylbi 209 |
. . . . . 6
⊢ (𝐺 Struct 𝑋 → (𝐼 ∈ ℕ → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ)))) |
42 | 41 | imp 396 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))) |
43 | 42 | 3adant2 1162 |
. . . 4
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → ⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩ ∈ ( ≤ ∩ (ℕ ×
ℕ))) |
44 | | structex 16195 |
. . . . . . 7
⊢ (𝐺 Struct 𝑋 → 𝐺 ∈ V) |
45 | | structn0fun 16196 |
. . . . . . 7
⊢ (𝐺 Struct 𝑋 → Fun (𝐺 ∖ {∅})) |
46 | 44, 45 | jca 508 |
. . . . . 6
⊢ (𝐺 Struct 𝑋 → (𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅}))) |
47 | 46 | 3ad2ant1 1164 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → (𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅}))) |
48 | | simp3 1169 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → 𝐼 ∈ ℕ) |
49 | | simp2 1168 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → 𝐸 ∈ 𝑉) |
50 | | setsfun0 16220 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ Fun (𝐺 ∖ {∅})) ∧
(𝐼 ∈ ℕ ∧
𝐸 ∈ 𝑉)) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅})) |
51 | 47, 48, 49, 50 | syl12anc 866 |
. . . 4
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅})) |
52 | 44 | 3ad2ant1 1164 |
. . . . . . 7
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → 𝐺 ∈ V) |
53 | 52, 49 | jca 508 |
. . . . . 6
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → (𝐺 ∈ V ∧ 𝐸 ∈ 𝑉)) |
54 | | setsdm 16218 |
. . . . . 6
⊢ ((𝐺 ∈ V ∧ 𝐸 ∈ 𝑉) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) = (dom 𝐺 ∪ {𝐼})) |
55 | 53, 54 | syl 17 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) = (dom 𝐺 ∪ {𝐼})) |
56 | | fveq2 6411 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ →
(...‘𝑋) =
(...‘⟨(1^{st} ‘𝑋), (2^{nd} ‘𝑋)⟩)) |
57 | | df-ov 6881 |
. . . . . . . . . . . . . . . . 17
⊢
((1^{st} ‘𝑋)...(2^{nd} ‘𝑋)) = (...‘⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩) |
58 | 56, 57 | syl6eqr 2851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ →
(...‘𝑋) =
((1^{st} ‘𝑋)...(2^{nd} ‘𝑋))) |
59 | 58 | sseq2d 3829 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ → (dom
𝐺 ⊆ (...‘𝑋) ↔ dom 𝐺 ⊆ ((1^{st} ‘𝑋)...(2^{nd} ‘𝑋)))) |
60 | 59 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (dom 𝐺 ⊆ (...‘𝑋) ↔ dom 𝐺 ⊆ ((1^{st} ‘𝑋)...(2^{nd} ‘𝑋)))) |
61 | | df-3an 1110 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ
∧ 𝐼 ∈ ℕ)
↔ (((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ 𝐼 ∈
ℕ)) |
62 | | nnz 11689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1^{st} ‘𝑋) ∈ ℕ → (1^{st}
‘𝑋) ∈
ℤ) |
63 | | nnz 11689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2^{nd} ‘𝑋) ∈ ℕ → (2^{nd}
‘𝑋) ∈
ℤ) |
64 | | nnz 11689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ ℕ → 𝐼 ∈
ℤ) |
65 | 62, 63, 64 | 3anim123i 1191 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ
∧ 𝐼 ∈ ℕ)
→ ((1^{st} ‘𝑋) ∈ ℤ ∧ (2^{nd}
‘𝑋) ∈ ℤ
∧ 𝐼 ∈
ℤ)) |
66 | | ssfzunsnext 12640 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) ∧
((1^{st} ‘𝑋)
∈ ℤ ∧ (2^{nd} ‘𝑋) ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (dom 𝐺 ∪ {𝐼}) ⊆ (if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋))...if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼))) |
67 | | df-ov 6881 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋))...if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)) = (...‘⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) |
68 | 66, 67 | syl6sseq 3847 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) ∧
((1^{st} ‘𝑋)
∈ ℤ ∧ (2^{nd} ‘𝑋) ∈ ℤ ∧ 𝐼 ∈ ℤ)) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
69 | 65, 68 | sylan2 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ ∧ 𝐼 ∈ ℕ)) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
70 | 69 | ex 402 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) →
(((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ ∧ 𝐼 ∈ ℕ) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
71 | 61, 70 | syl5bir 235 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) →
((((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
∧ 𝐼 ∈ ℕ)
→ (dom 𝐺 ∪ {𝐼}) ⊆
(...‘⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩))) |
72 | 71 | expd 405 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝐺 ⊆ ((1^{st}
‘𝑋)...(2^{nd}
‘𝑋)) →
(((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
73 | 72 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
(((1^{st} ‘𝑋) ∈ ℕ ∧ (2^{nd}
‘𝑋) ∈ ℕ)
→ (dom 𝐺 ⊆
((1^{st} ‘𝑋)...(2^{nd} ‘𝑋)) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
74 | 73 | adantl 474 |
. . . . . . . . . . . . . 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} ‘𝑋), 𝐼)⟩)))) |
75 | 60, 74 | sylbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝑋 = ⟨(1^{st}
‘𝑋), (2^{nd}
‘𝑋)⟩ ∧
((1^{st} ‘𝑋)
∈ ℕ ∧ (2^{nd} ‘𝑋) ∈ ℕ)) → (dom 𝐺 ⊆ (...‘𝑋) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
76 | 3, 75 | sylbi 209 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (ℕ ×
ℕ) → (dom 𝐺
⊆ (...‘𝑋)
→ (𝐼 ∈ ℕ
→ (dom 𝐺 ∪ {𝐼}) ⊆
(...‘⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩)))) |
77 | 76 | adantl 474 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ≤ ∧ 𝑋 ∈ (ℕ ×
ℕ)) → (dom 𝐺
⊆ (...‘𝑋)
→ (𝐼 ∈ ℕ
→ (dom 𝐺 ∪ {𝐼}) ⊆
(...‘⟨if(𝐼 ≤
(1^{st} ‘𝑋),
𝐼, (1^{st}
‘𝑋)), if(𝐼 ≤ (2^{nd}
‘𝑋), (2^{nd}
‘𝑋), 𝐼)⟩)))) |
78 | 2, 77 | sylbi 209 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) → (dom 𝐺 ⊆ (...‘𝑋) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)))) |
79 | 78 | imp 396 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ dom 𝐺 ⊆ (...‘𝑋)) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
80 | 79 | 3adant2 1162 |
. . . . . . . 8
⊢ ((𝑋 ∈ ( ≤ ∩ (ℕ
× ℕ)) ∧ Fun (𝐺 ∖ {∅}) ∧ dom 𝐺 ⊆ (...‘𝑋)) → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
81 | 1, 80 | sylbi 209 |
. . . . . . 7
⊢ (𝐺 Struct 𝑋 → (𝐼 ∈ ℕ → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩))) |
82 | 81 | imp 396 |
. . . . . 6
⊢ ((𝐺 Struct 𝑋 ∧ 𝐼 ∈ ℕ) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
83 | 82 | 3adant2 1162 |
. . . . 5
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → (dom 𝐺 ∪ {𝐼}) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
84 | 55, 83 | eqsstrd 3835 |
. . . 4
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → dom (𝐺 sSet ⟨𝐼, 𝐸⟩) ⊆ (...‘⟨if(𝐼 ≤ (1^{st}
‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩)) |
85 | | isstruct2 16194 |
. . . 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} ‘𝑋), 𝐼)⟩))) |
86 | 43, 51, 84, 85 | syl3anbrc 1444 |
. . 3
⊢ ((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) → (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) |
87 | 86 | adantr 473 |
. 2
⊢ (((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) ∧ 𝑌 = ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) → (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) |
88 | | breq2 4847 |
. . 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} ‘𝑋), 𝐼)⟩)) |
89 | 88 | adantl 474 |
. 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} ‘𝑋), 𝐼)⟩)) |
90 | 87, 89 | mpbird 249 |
1
⊢ (((𝐺 Struct 𝑋 ∧ 𝐸 ∈ 𝑉 ∧ 𝐼 ∈ ℕ) ∧ 𝑌 = ⟨if(𝐼 ≤ (1^{st} ‘𝑋), 𝐼, (1^{st} ‘𝑋)), if(𝐼 ≤ (2^{nd} ‘𝑋), (2^{nd} ‘𝑋), 𝐼)⟩) → (𝐺 sSet ⟨𝐼, 𝐸⟩) Struct 𝑌) |