Step | Hyp | Ref
| Expression |
1 | | frpoins3xp3g.2 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓)) |
2 | 1 | sbcbidv 3798 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → ([(2nd ‘𝑞) / 𝑧]𝜑 ↔ [(2nd ‘𝑞) / 𝑧]𝜓)) |
3 | 2 | sbcbidv 3798 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → ([(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓)) |
4 | 3 | cbvsbcvw 3774 |
. . . . . . 7
⊢
([(1st ‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 ↔ [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓) |
5 | | frpoins3xp3g.3 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒)) |
6 | 5 | sbcbidv 3798 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑡 → ([(2nd ‘𝑞) / 𝑧]𝜓 ↔ [(2nd ‘𝑞) / 𝑧]𝜒)) |
7 | 6 | cbvsbcvw 3774 |
. . . . . . . . 9
⊢
([(2nd ‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑧]𝜒) |
8 | | frpoins3xp3g.4 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃)) |
9 | 8 | cbvsbcvw 3774 |
. . . . . . . . . 10
⊢
([(2nd ‘𝑞) / 𝑧]𝜒 ↔ [(2nd ‘𝑞) / 𝑢]𝜃) |
10 | 9 | sbcbii 3799 |
. . . . . . . . 9
⊢
([(2nd ‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑧]𝜒 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
11 | 7, 10 | bitri 274 |
. . . . . . . 8
⊢
([(2nd ‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
12 | 11 | sbcbii 3799 |
. . . . . . 7
⊢
([(1st ‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓 ↔ [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
13 | 4, 12 | bitri 274 |
. . . . . 6
⊢
([(1st ‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 ↔ [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
14 | 13 | ralbii 3096 |
. . . . 5
⊢
(∀𝑞 ∈
Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
15 | | el2xptp 7967 |
. . . . . 6
⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉) |
16 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
17 | | nfsbc1v 3759 |
. . . . . . . 8
⊢
Ⅎ𝑥[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
18 | 16, 17 | nfim 1899 |
. . . . . . 7
⊢
Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) |
19 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑥 ∈ 𝐴 |
20 | | nfv 1917 |
. . . . . . . . 9
⊢
Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
21 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(1st ‘(1st
‘𝑝)) |
22 | | nfsbc1v 3759 |
. . . . . . . . . 10
⊢
Ⅎ𝑦[(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
23 | 21, 22 | nfsbcw 3761 |
. . . . . . . . 9
⊢
Ⅎ𝑦[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
24 | 20, 23 | nfim 1899 |
. . . . . . . 8
⊢
Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) |
25 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
26 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
27 | | nfcv 2907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧(1st ‘(1st
‘𝑝)) |
28 | | nfcv 2907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧(2nd ‘(1st
‘𝑝)) |
29 | | nfsbc1v 3759 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧[(2nd ‘𝑝) / 𝑧]𝜑 |
30 | 28, 29 | nfsbcw 3761 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧[(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
31 | 27, 30 | nfsbcw 3761 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
32 | 26, 31 | nfim 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) |
33 | | predss 6261 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ⊆ ((𝐴 × 𝐵) × 𝐶) |
34 | | sseqin2 4175 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) |
35 | 33, 34 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) |
36 | 35 | eleq2i 2829 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) |
37 | 36 | bicomi 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
38 | | elin 3926 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
39 | 37, 38 | bitri 274 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
40 | 39 | imbi1i 349 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
41 | | impexp 451 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
42 | 40, 41 | bitri 274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
43 | 42 | albii 1821 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
44 | 43 | bicomi 223 |
. . . . . . . . . . . . . 14
⊢
(∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
45 | | r3al 3193 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
46 | | nfv 1917 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) |
47 | | nfsbc1v 3759 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑤[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
48 | 46, 47 | nfim 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
49 | | nfv 1917 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) |
50 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡(1st ‘(1st
‘𝑞)) |
51 | | nfsbc1v 3759 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡[(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
52 | 50, 51 | nfsbcw 3761 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
53 | 49, 52 | nfim 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
54 | | nfv 1917 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) |
55 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑢(1st ‘(1st
‘𝑞)) |
56 | | nfcv 2907 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑢(2nd ‘(1st
‘𝑞)) |
57 | | nfsbc1v 3759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑢[(2nd ‘𝑞) / 𝑢]𝜃 |
58 | 56, 57 | nfsbcw 3761 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑢[(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
59 | 55, 58 | nfsbcw 3761 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑢[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
60 | 54, 59 | nfim 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
61 | | nfv 1917 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑞(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) |
62 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = 〈𝑤, 𝑡, 𝑢〉 → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ↔ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
63 | | sbcoteq1a 7983 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = 〈𝑤, 𝑡, 𝑢〉 → ([(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 ↔ 𝜃)) |
64 | 62, 63 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 = 〈𝑤, 𝑡, 𝑢〉 → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
65 | 48, 53, 60, 61, 64 | ralxp3f 8069 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑞 ∈
((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃)) |
66 | | elin 3926 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑤, 𝑡, 𝑢〉 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ (〈𝑤, 𝑡, 𝑢〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
67 | 35 | eleq2i 2829 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑤, 𝑡, 𝑢〉 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) |
68 | | otelxp 5676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑤, 𝑡, 𝑢〉 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶)) |
69 | 68 | anbi1i 624 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑤, 𝑡, 𝑢〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
70 | 66, 67, 69 | 3bitr3i 300 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
71 | 70 | imbi1i 349 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ (((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) → 𝜃)) |
72 | | impexp 451 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
73 | 71, 72 | bitri 274 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
74 | 73 | 3albii 1823 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
75 | 45, 65, 74 | 3bitr4ri 303 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
76 | | df-ral 3065 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑞 ∈
((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
77 | 75, 76 | bitri 274 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
78 | | df-ral 3065 |
. . . . . . . . . . . . . 14
⊢
(∀𝑞 ∈
Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
79 | 44, 77, 78 | 3bitr4ri 303 |
. . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃)) |
80 | | frpoins3xp3g.1 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) → 𝜑)) |
81 | 79, 80 | biimtrid 241 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → 𝜑)) |
82 | | predeq3 6257 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) |
83 | 82 | raleqdv 3313 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
84 | | sbcoteq1a 7983 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → ([(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 ↔ 𝜑)) |
85 | 83, 84 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → ((∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) ↔ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → 𝜑))) |
86 | 81, 85 | syl5ibrcom 246 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑))) |
87 | 86 | 3expia 1121 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐶 → (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)))) |
88 | 25, 32, 87 | rexlimd 3249 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑))) |
89 | 88 | ex 413 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)))) |
90 | 19, 24, 89 | rexlimd 3249 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑))) |
91 | 18, 90 | rexlimi 3242 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)) |
92 | 15, 91 | sylbi 216 |
. . . . 5
⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)) |
93 | 14, 92 | biimtrid 241 |
. . . 4
⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)) |
94 | | 2fveq3 6847 |
. . . . 5
⊢ (𝑝 = 𝑞 → (1st
‘(1st ‘𝑝)) = (1st ‘(1st
‘𝑞))) |
95 | | 2fveq3 6847 |
. . . . . 6
⊢ (𝑝 = 𝑞 → (2nd
‘(1st ‘𝑝)) = (2nd ‘(1st
‘𝑞))) |
96 | | fveq2 6842 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → (2nd ‘𝑝) = (2nd ‘𝑞)) |
97 | 96 | sbceq1d 3744 |
. . . . . 6
⊢ (𝑝 = 𝑞 → ([(2nd ‘𝑝) / 𝑧]𝜑 ↔ [(2nd ‘𝑞) / 𝑧]𝜑)) |
98 | 95, 97 | sbceqbid 3746 |
. . . . 5
⊢ (𝑝 = 𝑞 → ([(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑)) |
99 | 94, 98 | sbceqbid 3746 |
. . . 4
⊢ (𝑝 = 𝑞 → ([(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 ↔ [(1st
‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑)) |
100 | 93, 99 | frpoins2g 6299 |
. . 3
⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) |
101 | | ralxp3es 8071 |
. . 3
⊢
(∀𝑝 ∈
((𝐴 × 𝐵) × 𝐶)[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑) |
102 | 100, 101 | sylib 217 |
. 2
⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑) |
103 | | frpoins3xp3g.5 |
. . 3
⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜏)) |
104 | | frpoins3xp3g.6 |
. . 3
⊢ (𝑦 = 𝑌 → (𝜏 ↔ 𝜂)) |
105 | | frpoins3xp3g.7 |
. . 3
⊢ (𝑧 = 𝑍 → (𝜂 ↔ 𝜁)) |
106 | 103, 104,
105 | rspc3v 3593 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → 𝜁)) |
107 | 102, 106 | mpan9 507 |
1
⊢ (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜁) |