Step | Hyp | Ref
| Expression |
1 | | brwdom3i 9340 |
. . 3
⊢ (𝐴 ≼* 𝐵 → ∃𝑓∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏)) |
2 | 1 | adantr 481 |
. 2
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → ∃𝑓∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏)) |
3 | | brwdom3i 9340 |
. . 3
⊢ (𝐶 ≼* 𝐷 → ∃𝑔∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) |
4 | 3 | adantl 482 |
. 2
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → ∃𝑔∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) |
5 | | relwdom 9323 |
. . . . . . . . . 10
⊢ Rel
≼* |
6 | 5 | brrelex1i 5645 |
. . . . . . . . 9
⊢ (𝐴 ≼* 𝐵 → 𝐴 ∈ V) |
7 | 5 | brrelex1i 5645 |
. . . . . . . . 9
⊢ (𝐶 ≼* 𝐷 → 𝐶 ∈ V) |
8 | | xpexg 7600 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 × 𝐶) ∈ V) |
9 | 6, 7, 8 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (𝐴 × 𝐶) ∈ V) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) ∧ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑))) → (𝐴 × 𝐶) ∈ V) |
11 | 5 | brrelex2i 5646 |
. . . . . . . . 9
⊢ (𝐴 ≼* 𝐵 → 𝐵 ∈ V) |
12 | 5 | brrelex2i 5646 |
. . . . . . . . 9
⊢ (𝐶 ≼* 𝐷 → 𝐷 ∈ V) |
13 | | xpexg 7600 |
. . . . . . . . 9
⊢ ((𝐵 ∈ V ∧ 𝐷 ∈ V) → (𝐵 × 𝐷) ∈ V) |
14 | 11, 12, 13 | syl2an 596 |
. . . . . . . 8
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (𝐵 × 𝐷) ∈ V) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) ∧ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑))) → (𝐵 × 𝐷) ∈ V) |
16 | | pm3.2 470 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑏 ∈
𝐵 𝑎 = (𝑓‘𝑏) → (∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → (∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)))) |
17 | 16 | ralimdv 3109 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑏 ∈
𝐵 𝑎 = (𝑓‘𝑏) → (∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → ∀𝑐 ∈ 𝐶 (∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)))) |
18 | 17 | com12 32 |
. . . . . . . . . . . . . 14
⊢
(∀𝑐 ∈
𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → (∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) → ∀𝑐 ∈ 𝐶 (∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)))) |
19 | 18 | ralimdv 3109 |
. . . . . . . . . . . . 13
⊢
(∀𝑐 ∈
𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐶 (∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)))) |
20 | 19 | impcom 408 |
. . . . . . . . . . . 12
⊢
((∀𝑎 ∈
𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐶 (∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑))) |
21 | | pm3.2 470 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (𝑓‘𝑏) → (𝑐 = (𝑔‘𝑑) → (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑)))) |
22 | 21 | reximdv 3201 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑓‘𝑏) → (∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → ∃𝑑 ∈ 𝐷 (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑)))) |
23 | 22 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑑 ∈
𝐷 𝑐 = (𝑔‘𝑑) → (𝑎 = (𝑓‘𝑏) → ∃𝑑 ∈ 𝐷 (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑)))) |
24 | 23 | reximdv 3201 |
. . . . . . . . . . . . . 14
⊢
(∃𝑑 ∈
𝐷 𝑐 = (𝑔‘𝑑) → (∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) → ∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑)))) |
25 | 24 | impcom 408 |
. . . . . . . . . . . . 13
⊢
((∃𝑏 ∈
𝐵 𝑎 = (𝑓‘𝑏) ∧ ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) → ∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑))) |
26 | 25 | 2ralimi 3088 |
. . . . . . . . . . . 12
⊢
(∀𝑎 ∈
𝐴 ∀𝑐 ∈ 𝐶 (∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐶 ∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑))) |
27 | 20, 26 | syl 17 |
. . . . . . . . . . 11
⊢
((∀𝑎 ∈
𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐶 ∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑))) |
28 | | eqeq1 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝑎, 𝑐〉 → (𝑥 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉 ↔ 〈𝑎, 𝑐〉 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉)) |
29 | | vex 3435 |
. . . . . . . . . . . . . . 15
⊢ 𝑎 ∈ V |
30 | | vex 3435 |
. . . . . . . . . . . . . . 15
⊢ 𝑐 ∈ V |
31 | 29, 30 | opth 5393 |
. . . . . . . . . . . . . 14
⊢
(〈𝑎, 𝑐〉 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉 ↔ (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑))) |
32 | 28, 31 | bitrdi 287 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝑎, 𝑐〉 → (𝑥 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉 ↔ (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑)))) |
33 | 32 | 2rexbidv 3228 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑎, 𝑐〉 → (∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 𝑥 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉 ↔ ∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑)))) |
34 | 33 | ralxp 5752 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝐴 × 𝐶)∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 𝑥 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉 ↔ ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐶 ∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 (𝑎 = (𝑓‘𝑏) ∧ 𝑐 = (𝑔‘𝑑))) |
35 | 27, 34 | sylibr 233 |
. . . . . . . . . 10
⊢
((∀𝑎 ∈
𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) → ∀𝑥 ∈ (𝐴 × 𝐶)∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 𝑥 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉) |
36 | 35 | r19.21bi 3134 |
. . . . . . . . 9
⊢
(((∀𝑎 ∈
𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) ∧ 𝑥 ∈ (𝐴 × 𝐶)) → ∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 𝑥 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉) |
37 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑏 ∈ V |
38 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑑 ∈ V |
39 | 37, 38 | op1std 7841 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 〈𝑏, 𝑑〉 → (1st ‘𝑦) = 𝑏) |
40 | 39 | fveq2d 6780 |
. . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑏, 𝑑〉 → (𝑓‘(1st ‘𝑦)) = (𝑓‘𝑏)) |
41 | 37, 38 | op2ndd 7842 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 〈𝑏, 𝑑〉 → (2nd ‘𝑦) = 𝑑) |
42 | 41 | fveq2d 6780 |
. . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑏, 𝑑〉 → (𝑔‘(2nd ‘𝑦)) = (𝑔‘𝑑)) |
43 | 40, 42 | opeq12d 4814 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑏, 𝑑〉 → 〈(𝑓‘(1st ‘𝑦)), (𝑔‘(2nd ‘𝑦))〉 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉) |
44 | 43 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑦 = 〈𝑏, 𝑑〉 → (𝑥 = 〈(𝑓‘(1st ‘𝑦)), (𝑔‘(2nd ‘𝑦))〉 ↔ 𝑥 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉)) |
45 | 44 | rexxp 5753 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
(𝐵 × 𝐷)𝑥 = 〈(𝑓‘(1st ‘𝑦)), (𝑔‘(2nd ‘𝑦))〉 ↔ ∃𝑏 ∈ 𝐵 ∃𝑑 ∈ 𝐷 𝑥 = 〈(𝑓‘𝑏), (𝑔‘𝑑)〉) |
46 | 36, 45 | sylibr 233 |
. . . . . . . 8
⊢
(((∀𝑎 ∈
𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑)) ∧ 𝑥 ∈ (𝐴 × 𝐶)) → ∃𝑦 ∈ (𝐵 × 𝐷)𝑥 = 〈(𝑓‘(1st ‘𝑦)), (𝑔‘(2nd ‘𝑦))〉) |
47 | 46 | adantll 711 |
. . . . . . 7
⊢ ((((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) ∧ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑))) ∧ 𝑥 ∈ (𝐴 × 𝐶)) → ∃𝑦 ∈ (𝐵 × 𝐷)𝑥 = 〈(𝑓‘(1st ‘𝑦)), (𝑔‘(2nd ‘𝑦))〉) |
48 | 10, 15, 47 | wdom2d 9337 |
. . . . . 6
⊢ (((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) ∧ (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) ∧ ∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑))) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷)) |
49 | 48 | expr 457 |
. . . . 5
⊢ (((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏)) → (∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷))) |
50 | 49 | exlimdv 1936 |
. . . 4
⊢ (((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) ∧ ∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏)) → (∃𝑔∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷))) |
51 | 50 | ex 413 |
. . 3
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) → (∃𝑔∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷)))) |
52 | 51 | exlimdv 1936 |
. 2
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (∃𝑓∀𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑎 = (𝑓‘𝑏) → (∃𝑔∀𝑐 ∈ 𝐶 ∃𝑑 ∈ 𝐷 𝑐 = (𝑔‘𝑑) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷)))) |
53 | 2, 4, 52 | mp2d 49 |
1
⊢ ((𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷) → (𝐴 × 𝐶) ≼* (𝐵 × 𝐷)) |