Step | Hyp | Ref
| Expression |
1 | | ssel 3141 |
. . 3
⊢ (𝐴 ⊆ 𝐵 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) |
2 | 1 | alrimivv 1868 |
. 2
⊢ (𝐴 ⊆ 𝐵 → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) |
3 | | eleq1 2233 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐴)) |
4 | | eleq1 2233 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ 𝐵 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵)) |
5 | 3, 4 | imbi12d 233 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵) ↔ (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) |
6 | 5 | biimprcd 159 |
. . . . . . . . 9
⊢
((〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) → (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))) |
7 | 6 | 2alimi 1449 |
. . . . . . . 8
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) → ∀𝑥∀𝑦(𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))) |
8 | | 19.23vv 1877 |
. . . . . . . 8
⊢
(∀𝑥∀𝑦(𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)) ↔ (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))) |
9 | 7, 8 | sylib 121 |
. . . . . . 7
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) → (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))) |
10 | 9 | com23 78 |
. . . . . 6
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) → (𝑧 ∈ 𝐴 → (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 → 𝑧 ∈ 𝐵))) |
11 | 10 | a2d 26 |
. . . . 5
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) → ((𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → (𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))) |
12 | 11 | alimdv 1872 |
. . . 4
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) → (∀𝑧(𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) → ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵))) |
13 | | df-rel 4618 |
. . . . 5
⊢ (Rel
𝐴 ↔ 𝐴 ⊆ (V × V)) |
14 | | dfss2 3136 |
. . . . 5
⊢ (𝐴 ⊆ (V × V) ↔
∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V))) |
15 | | elvv 4673 |
. . . . . . 7
⊢ (𝑧 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) |
16 | 15 | imbi2i 225 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)) ↔ (𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) |
17 | 16 | albii 1463 |
. . . . 5
⊢
(∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)) ↔ ∀𝑧(𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) |
18 | 13, 14, 17 | 3bitri 205 |
. . . 4
⊢ (Rel
𝐴 ↔ ∀𝑧(𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉)) |
19 | | dfss2 3136 |
. . . 4
⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑧(𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵)) |
20 | 12, 18, 19 | 3imtr4g 204 |
. . 3
⊢
(∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) → (Rel 𝐴 → 𝐴 ⊆ 𝐵)) |
21 | 20 | com12 30 |
. 2
⊢ (Rel
𝐴 → (∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵) → 𝐴 ⊆ 𝐵)) |
22 | 2, 21 | impbid2 142 |
1
⊢ (Rel
𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) |