Step | Hyp | Ref
| Expression |
1 | | elxp2 5549 |
. . . . . 6
⊢ (𝑝 ∈ (𝐴 × 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑝 = 〈𝑥, 𝑦〉) |
2 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑥Pred(𝑅, (𝐴 × 𝐵), 𝑝) |
3 | | nfsbc1v 3700 |
. . . . . . . . 9
⊢
Ⅎ𝑥[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 |
4 | 2, 3 | nfralw 3138 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 |
5 | | nfsbc1v 3700 |
. . . . . . . 8
⊢
Ⅎ𝑥[(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑 |
6 | 4, 5 | nfim 1903 |
. . . . . . 7
⊢
Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑) |
7 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑥 ∈ 𝐴 |
8 | | nfcv 2899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦Pred(𝑅, (𝐴 × 𝐵), 𝑝) |
9 | | nfcv 2899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(1st ‘𝑞) |
10 | | nfsbc1v 3700 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦[(2nd ‘𝑞) / 𝑦]𝜑 |
11 | 9, 10 | nfsbcw 3702 |
. . . . . . . . . 10
⊢
Ⅎ𝑦[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 |
12 | 8, 11 | nfralw 3138 |
. . . . . . . . 9
⊢
Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 |
13 | | nfcv 2899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(1st ‘𝑝) |
14 | | nfsbc1v 3700 |
. . . . . . . . . 10
⊢
Ⅎ𝑦[(2nd ‘𝑝) / 𝑦]𝜑 |
15 | 13, 14 | nfsbcw 3702 |
. . . . . . . . 9
⊢
Ⅎ𝑦[(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑 |
16 | 12, 15 | nfim 1903 |
. . . . . . . 8
⊢
Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑) |
17 | | frpoins3xpg.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) |
18 | 17 | sbcbidv 3736 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ([(2nd ‘𝑞) / 𝑦]𝜑 ↔ [(2nd ‘𝑞) / 𝑦]𝜓)) |
19 | 18 | cbvsbcvw 3715 |
. . . . . . . . . . . . . 14
⊢
([(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ [(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑦]𝜓) |
20 | | frpoins3xpg.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒)) |
21 | 20 | cbvsbcvw 3715 |
. . . . . . . . . . . . . . 15
⊢
([(2nd ‘𝑞) / 𝑦]𝜓 ↔ [(2nd ‘𝑞) / 𝑤]𝜒) |
22 | 21 | sbcbii 3738 |
. . . . . . . . . . . . . 14
⊢
([(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑦]𝜓 ↔ [(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒) |
23 | 19, 22 | bitri 278 |
. . . . . . . . . . . . 13
⊢
([(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ [(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒) |
24 | 23 | ralbii 3080 |
. . . . . . . . . . . 12
⊢
(∀𝑞 ∈
Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒) |
25 | | impexp 454 |
. . . . . . . . . . . . . . 15
⊢ (((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ (𝑞 ∈ (𝐴 × 𝐵) → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒))) |
26 | | elin 3859 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉))) |
27 | | predss 6136 |
. . . . . . . . . . . . . . . . . . 19
⊢
Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) ⊆ (𝐴 × 𝐵) |
28 | | sseqin2 4106 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) ⊆ (𝐴 × 𝐵) ↔ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) = Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) |
29 | 27, 28 | mpbi 233 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) = Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) |
30 | 29 | eleq2i 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) |
31 | 26, 30 | bitr3i 280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) |
32 | 31 | imbi1i 353 |
. . . . . . . . . . . . . . 15
⊢ (((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) |
33 | 25, 32 | bitr3i 280 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ (𝐴 × 𝐵) → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) ↔ (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) |
34 | 33 | albii 1826 |
. . . . . . . . . . . . 13
⊢
(∀𝑞(𝑞 ∈ (𝐴 × 𝐵) → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) |
35 | | df-ral 3058 |
. . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
(𝐴 × 𝐵)(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ ∀𝑞(𝑞 ∈ (𝐴 × 𝐵) → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒))) |
36 | | df-ral 3058 |
. . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) |
37 | 34, 35, 36 | 3bitr4ri 307 |
. . . . . . . . . . . 12
⊢
(∀𝑞 ∈
Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒 ↔ ∀𝑞 ∈ (𝐴 × 𝐵)(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) |
38 | | nfv 1921 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) |
39 | | nfsbc1v 3700 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒 |
40 | 38, 39 | nfim 1903 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑧(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) |
41 | | nfv 1921 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) |
42 | | nfcv 2899 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑤(1st ‘𝑞) |
43 | | nfsbc1v 3700 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑤[(2nd ‘𝑞) / 𝑤]𝜒 |
44 | 42, 43 | nfsbcw 3702 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒 |
45 | 41, 44 | nfim 1903 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑤(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) |
46 | | nfv 1921 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑞(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒) |
47 | | eleq1 2820 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 〈𝑧, 𝑤〉 → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) ↔ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉))) |
48 | | sbcopeq1a 7773 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 〈𝑧, 𝑤〉 → ([(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒 ↔ 𝜒)) |
49 | 47, 48 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 〈𝑧, 𝑤〉 → ((𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) |
50 | 40, 45, 46, 49 | ralxpf 5689 |
. . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
(𝐴 × 𝐵)(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) |
51 | | r2al 3113 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐵 (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) |
52 | | impexp 454 |
. . . . . . . . . . . . . . . 16
⊢
(((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → 𝜒) ↔ (〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) |
53 | | opelxp 5561 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) |
54 | 53 | imbi1i 353 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) |
55 | 52, 54 | bitri 278 |
. . . . . . . . . . . . . . 15
⊢
(((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → 𝜒) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) |
56 | | elin 3859 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑧, 𝑤〉 ∈ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ (〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉))) |
57 | 29 | eleq2i 2824 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑧, 𝑤〉 ∈ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) |
58 | 56, 57 | bitr3i 280 |
. . . . . . . . . . . . . . . 16
⊢
((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) |
59 | 58 | imbi1i 353 |
. . . . . . . . . . . . . . 15
⊢
(((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → 𝜒) ↔ (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) |
60 | 55, 59 | bitr3i 280 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) ↔ (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) |
61 | 60 | 2albii 1827 |
. . . . . . . . . . . . 13
⊢
(∀𝑧∀𝑤((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) ↔ ∀𝑧∀𝑤(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) |
62 | 50, 51, 61 | 3bitri 300 |
. . . . . . . . . . . 12
⊢
(∀𝑞 ∈
(𝐴 × 𝐵)(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ ∀𝑧∀𝑤(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) |
63 | 24, 37, 62 | 3bitri 300 |
. . . . . . . . . . 11
⊢
(∀𝑞 ∈
Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ ∀𝑧∀𝑤(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) |
64 | | frpoins3xpg.1 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑧∀𝑤(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒) → 𝜑)) |
65 | 63, 64 | syl5bi 245 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → 𝜑)) |
66 | | predeq3 6133 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → Pred(𝑅, (𝐴 × 𝐵), 𝑝) = Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) |
67 | 66 | raleqdv 3316 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑)) |
68 | | sbcopeq1a 7773 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → ([(1st
‘𝑝) / 𝑥][(2nd
‘𝑝) / 𝑦]𝜑 ↔ 𝜑)) |
69 | 67, 68 | imbi12d 348 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑥, 𝑦〉 → ((∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑) ↔ (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → 𝜑))) |
70 | 65, 69 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑))) |
71 | 70 | ex 416 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑)))) |
72 | 7, 16, 71 | rexlimd 3227 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑))) |
73 | 6, 72 | rexlimi 3225 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑)) |
74 | 1, 73 | sylbi 220 |
. . . . 5
⊢ (𝑝 ∈ (𝐴 × 𝐵) → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑)) |
75 | | fveq2 6674 |
. . . . . 6
⊢ (𝑝 = 𝑞 → (1st ‘𝑝) = (1st ‘𝑞)) |
76 | | fveq2 6674 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → (2nd ‘𝑝) = (2nd ‘𝑞)) |
77 | 76 | sbceq1d 3685 |
. . . . . 6
⊢ (𝑝 = 𝑞 → ([(2nd ‘𝑝) / 𝑦]𝜑 ↔ [(2nd ‘𝑞) / 𝑦]𝜑)) |
78 | 75, 77 | sbceqbid 3687 |
. . . . 5
⊢ (𝑝 = 𝑞 → ([(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑 ↔ [(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑)) |
79 | 74, 78 | frpoins2g 33388 |
. . . 4
⊢ ((𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵)) → ∀𝑝 ∈ (𝐴 × 𝐵)[(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑) |
80 | | ralxpes 33252 |
. . . 4
⊢
(∀𝑝 ∈
(𝐴 × 𝐵)[(1st
‘𝑝) / 𝑥][(2nd
‘𝑝) / 𝑦]𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) |
81 | 79, 80 | sylib 221 |
. . 3
⊢ ((𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) |
82 | | frpoins3xpg.4 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜃)) |
83 | | frpoins3xpg.5 |
. . . 4
⊢ (𝑦 = 𝑌 → (𝜃 ↔ 𝜏)) |
84 | 82, 83 | rspc2va 3537 |
. . 3
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) → 𝜏) |
85 | 81, 84 | sylan2 596 |
. 2
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵))) → 𝜏) |
86 | 85 | ancoms 462 |
1
⊢ (((𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → 𝜏) |