Step | Hyp | Ref
| Expression |
1 | | ssel 2933 |
. . . 4
⊢ (𝑅 ⊆ 𝑆 → (〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆)) |
2 | 1 | a1d 22 |
. . 3
⊢ (𝑅 ⊆ 𝑆 → ((x ∈ A ∧ y ∈ B) → (〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆))) |
3 | 2 | ralrimivv 2394 |
. 2
⊢ (𝑅 ⊆ 𝑆 → ∀x ∈ A ∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆)) |
4 | | eleq1 2097 |
. . . . . . . . . . . 12
⊢ (z = 〈x,
y〉 → (z ∈ 𝑅 ↔ 〈x, y〉 ∈ 𝑅)) |
5 | | eleq1 2097 |
. . . . . . . . . . . 12
⊢ (z = 〈x,
y〉 → (z ∈ 𝑆 ↔ 〈x, y〉 ∈ 𝑆)) |
6 | 4, 5 | imbi12d 223 |
. . . . . . . . . . 11
⊢ (z = 〈x,
y〉 → ((z ∈ 𝑅 → z ∈ 𝑆) ↔ (〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆))) |
7 | 6 | biimprcd 149 |
. . . . . . . . . 10
⊢
((〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆) → (z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆))) |
8 | 7 | ralimi 2378 |
. . . . . . . . 9
⊢ (∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆) → ∀y ∈ B (z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆))) |
9 | 8 | ralimi 2378 |
. . . . . . . 8
⊢ (∀x ∈ A ∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆) → ∀x ∈ A ∀y ∈ B (z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆))) |
10 | | r19.23v 2419 |
. . . . . . . . . 10
⊢ (∀y ∈ B (z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ (∃y ∈ B z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆))) |
11 | 10 | ralbii 2324 |
. . . . . . . . 9
⊢ (∀x ∈ A ∀y ∈ B (z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ ∀x ∈ A (∃y ∈ B z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆))) |
12 | | r19.23v 2419 |
. . . . . . . . 9
⊢ (∀x ∈ A (∃y ∈ B z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ (∃x ∈ A ∃y ∈ B z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆))) |
13 | 11, 12 | bitri 173 |
. . . . . . . 8
⊢ (∀x ∈ A ∀y ∈ B (z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆)) ↔ (∃x ∈ A ∃y ∈ B z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆))) |
14 | 9, 13 | sylib 127 |
. . . . . . 7
⊢ (∀x ∈ A ∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆) → (∃x ∈ A ∃y ∈ B z = 〈x,
y〉 → (z ∈ 𝑅 → z ∈ 𝑆))) |
15 | 14 | com23 72 |
. . . . . 6
⊢ (∀x ∈ A ∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆) → (z ∈ 𝑅 → (∃x ∈ A ∃y ∈ B z = 〈x,
y〉 → z ∈ 𝑆))) |
16 | 15 | a2d 23 |
. . . . 5
⊢ (∀x ∈ A ∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆) → ((z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = 〈x,
y〉) → (z ∈ 𝑅 → z ∈ 𝑆))) |
17 | 16 | alimdv 1756 |
. . . 4
⊢ (∀x ∈ A ∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆) → (∀z(z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = 〈x,
y〉) → ∀z(z ∈ 𝑅 → z ∈ 𝑆))) |
18 | | dfss2 2928 |
. . . . 5
⊢ (𝑅 ⊆ (A × B)
↔ ∀z(z ∈ 𝑅 → z ∈ (A × B))) |
19 | | elxp2 4306 |
. . . . . . 7
⊢ (z ∈ (A × B)
↔ ∃x ∈ A ∃y ∈ B z =
〈x, y〉) |
20 | 19 | imbi2i 215 |
. . . . . 6
⊢
((z ∈ 𝑅 → z ∈ (A × B))
↔ (z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = 〈x,
y〉)) |
21 | 20 | albii 1356 |
. . . . 5
⊢ (∀z(z ∈ 𝑅 → z ∈ (A × B))
↔ ∀z(z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = 〈x,
y〉)) |
22 | 18, 21 | bitri 173 |
. . . 4
⊢ (𝑅 ⊆ (A × B)
↔ ∀z(z ∈ 𝑅 → ∃x ∈ A ∃y ∈ B z = 〈x,
y〉)) |
23 | | dfss2 2928 |
. . . 4
⊢ (𝑅 ⊆ 𝑆 ↔ ∀z(z ∈ 𝑅 → z ∈ 𝑆)) |
24 | 17, 22, 23 | 3imtr4g 194 |
. . 3
⊢ (∀x ∈ A ∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆) → (𝑅 ⊆ (A × B)
→ 𝑅 ⊆ 𝑆)) |
25 | 24 | com12 27 |
. 2
⊢ (𝑅 ⊆ (A × B)
→ (∀x ∈ A ∀y ∈ B (〈x,
y〉 ∈
𝑅 → 〈x, y〉 ∈ 𝑆) → 𝑅 ⊆ 𝑆)) |
26 | 3, 25 | impbid2 131 |
1
⊢ (𝑅 ⊆ (A × B)
→ (𝑅 ⊆ 𝑆 ↔ ∀x ∈ A ∀y ∈ B
(〈x, y〉 ∈ 𝑅 → 〈x, y〉 ∈ 𝑆))) |