Step | Hyp | Ref
| Expression |
1 | | ssel 2933 |
. . . 4
⊢ (A ⊆ B
→ (〈〈x, y〉, z〉
∈ A
→ 〈〈x, y〉, z〉
∈ B)) |
2 | 1 | alrimiv 1751 |
. . 3
⊢ (A ⊆ B
→ ∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B)) |
3 | 2 | alrimivv 1752 |
. 2
⊢ (A ⊆ B
→ ∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B)) |
4 | | elvvv 4346 |
. . . . . . . 8
⊢ (w ∈ ((V × V)
× V) ↔ ∃x∃y∃z w =
〈〈x, y〉, z〉) |
5 | | eleq1 2097 |
. . . . . . . . . . . . . 14
⊢ (w = 〈〈x, y〉,
z〉 → (w ∈ A ↔ 〈〈x, y〉,
z〉 ∈
A)) |
6 | | eleq1 2097 |
. . . . . . . . . . . . . 14
⊢ (w = 〈〈x, y〉,
z〉 → (w ∈ B ↔ 〈〈x, y〉,
z〉 ∈
B)) |
7 | 5, 6 | imbi12d 223 |
. . . . . . . . . . . . 13
⊢ (w = 〈〈x, y〉,
z〉 → ((w ∈ A → w ∈ B) ↔
(〈〈x, y〉, z〉
∈ A
→ 〈〈x, y〉, z〉
∈ B))) |
8 | 7 | biimprcd 149 |
. . . . . . . . . . . 12
⊢
((〈〈x, y〉, z〉
∈ A
→ 〈〈x, y〉, z〉
∈ B)
→ (w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B))) |
9 | 8 | alimi 1341 |
. . . . . . . . . . 11
⊢ (∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → ∀z(w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B))) |
10 | | 19.23v 1760 |
. . . . . . . . . . 11
⊢ (∀z(w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B)) ↔
(∃z
w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B))) |
11 | 9, 10 | sylib 127 |
. . . . . . . . . 10
⊢ (∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → (∃z w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B))) |
12 | 11 | 2alimi 1342 |
. . . . . . . . 9
⊢ (∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → ∀x∀y(∃z w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B))) |
13 | | 19.23vv 1761 |
. . . . . . . . 9
⊢ (∀x∀y(∃z w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B)) ↔
(∃x∃y∃z w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B))) |
14 | 12, 13 | sylib 127 |
. . . . . . . 8
⊢ (∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → (∃x∃y∃z w = 〈〈x, y〉,
z〉 → (w ∈ A → w ∈ B))) |
15 | 4, 14 | syl5bi 141 |
. . . . . . 7
⊢ (∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → (w ∈ ((V × V)
× V) → (w ∈ A →
w ∈
B))) |
16 | 15 | com23 72 |
. . . . . 6
⊢ (∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → (w ∈ A → (w
∈ ((V × V) × V) → w ∈ B))) |
17 | 16 | a2d 23 |
. . . . 5
⊢ (∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → ((w ∈ A → w ∈ ((V × V) × V)) → (w ∈ A → w ∈ B))) |
18 | 17 | alimdv 1756 |
. . . 4
⊢ (∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → (∀w(w ∈ A → w ∈ ((V × V) × V)) → ∀w(w ∈ A → w ∈ B))) |
19 | | dfss2 2928 |
. . . 4
⊢ (A ⊆ ((V × V) × V) ↔ ∀w(w ∈ A → w ∈ ((V × V) × V))) |
20 | | dfss2 2928 |
. . . 4
⊢ (A ⊆ B
↔ ∀w(w ∈ A →
w ∈
B)) |
21 | 18, 19, 20 | 3imtr4g 194 |
. . 3
⊢ (∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → (A ⊆ ((V × V) × V) → A ⊆ B)) |
22 | 21 | com12 27 |
. 2
⊢ (A ⊆ ((V × V) × V) → (∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B) → A ⊆ B)) |
23 | 3, 22 | impbid2 131 |
1
⊢ (A ⊆ ((V × V) × V) → (A ⊆ B
↔ ∀x∀y∀z(〈〈x,
y〉, z〉 ∈ A → 〈〈x, y〉,
z〉 ∈
B))) |