| Step | Hyp | Ref
| Expression |
| 1 | | frpoins3xp3g.2 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓)) |
| 2 | 1 | sbcbidv 3845 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → ([(2nd ‘𝑞) / 𝑧]𝜑 ↔ [(2nd ‘𝑞) / 𝑧]𝜓)) |
| 3 | 2 | sbcbidv 3845 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → ([(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓)) |
| 4 | 3 | cbvsbcvw 3822 |
. . . . . . 7
⊢
([(1st ‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 ↔ [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓) |
| 5 | | frpoins3xp3g.3 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒)) |
| 6 | 5 | sbcbidv 3845 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑡 → ([(2nd ‘𝑞) / 𝑧]𝜓 ↔ [(2nd ‘𝑞) / 𝑧]𝜒)) |
| 7 | 6 | cbvsbcvw 3822 |
. . . . . . . . 9
⊢
([(2nd ‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑧]𝜒) |
| 8 | | frpoins3xp3g.4 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃)) |
| 9 | 8 | cbvsbcvw 3822 |
. . . . . . . . . 10
⊢
([(2nd ‘𝑞) / 𝑧]𝜒 ↔ [(2nd ‘𝑞) / 𝑢]𝜃) |
| 10 | 9 | sbcbii 3846 |
. . . . . . . . 9
⊢
([(2nd ‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑧]𝜒 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
| 11 | 7, 10 | bitri 275 |
. . . . . . . 8
⊢
([(2nd ‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
| 12 | 11 | sbcbii 3846 |
. . . . . . 7
⊢
([(1st ‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜓 ↔ [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
| 13 | 4, 12 | bitri 275 |
. . . . . 6
⊢
([(1st ‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 ↔ [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
| 14 | 13 | ralbii 3093 |
. . . . 5
⊢
(∀𝑞 ∈
Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
| 15 | | el2xptp 8060 |
. . . . . 6
⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉) |
| 16 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
| 17 | | nfsbc1v 3808 |
. . . . . . . 8
⊢
Ⅎ𝑥[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
| 18 | 16, 17 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) |
| 19 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑦 𝑥 ∈ 𝐴 |
| 20 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
| 21 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(1st ‘(1st
‘𝑝)) |
| 22 | | nfsbc1v 3808 |
. . . . . . . . . 10
⊢
Ⅎ𝑦[(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
| 23 | 21, 22 | nfsbcw 3810 |
. . . . . . . . 9
⊢
Ⅎ𝑦[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
| 24 | 20, 23 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) |
| 25 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) |
| 26 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
| 27 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧(1st ‘(1st
‘𝑝)) |
| 28 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧(2nd ‘(1st
‘𝑝)) |
| 29 | | nfsbc1v 3808 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑧[(2nd ‘𝑝) / 𝑧]𝜑 |
| 30 | 28, 29 | nfsbcw 3810 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑧[(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
| 31 | 27, 30 | nfsbcw 3810 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 |
| 32 | 26, 31 | nfim 1896 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) |
| 33 | | predss 6329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ⊆ ((𝐴 × 𝐵) × 𝐶) |
| 34 | | sseqin2 4223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) |
| 35 | 33, 34 | mpbi 230 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) |
| 36 | 35 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) |
| 37 | 36 | bicomi 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
| 38 | | elin 3967 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
| 39 | 37, 38 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
| 40 | 39 | imbi1i 349 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
| 41 | | impexp 450 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
| 42 | 40, 41 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
| 43 | 42 | albii 1819 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
| 44 | 43 | bicomi 224 |
. . . . . . . . . . . . . 14
⊢
(∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
| 45 | | r3al 3197 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
| 46 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) |
| 47 | | nfsbc1v 3808 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑤[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
| 48 | 46, 47 | nfim 1896 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
| 49 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) |
| 50 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡(1st ‘(1st
‘𝑞)) |
| 51 | | nfsbc1v 3808 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡[(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
| 52 | 50, 51 | nfsbcw 3810 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
| 53 | 49, 52 | nfim 1896 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
| 54 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) |
| 55 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑢(1st ‘(1st
‘𝑞)) |
| 56 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑢(2nd ‘(1st
‘𝑞)) |
| 57 | | nfsbc1v 3808 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑢[(2nd ‘𝑞) / 𝑢]𝜃 |
| 58 | 56, 57 | nfsbcw 3810 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑢[(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
| 59 | 55, 58 | nfsbcw 3810 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑢[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 |
| 60 | 54, 59 | nfim 1896 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) |
| 61 | | nfv 1914 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑞(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) |
| 62 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = 〈𝑤, 𝑡, 𝑢〉 → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ↔ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
| 63 | | sbcoteq1a 8076 |
. . . . . . . . . . . . . . . . . 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 8162 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑞 ∈
((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃)) |
| 66 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑤, 𝑡, 𝑢〉 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ (〈𝑤, 𝑡, 𝑢〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
| 67 | 35 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑤, 𝑡, 𝑢〉 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) |
| 68 | | otelxp 5729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈𝑤, 𝑡, 𝑢〉 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶)) |
| 69 | 68 | anbi1i 624 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((〈𝑤, 𝑡, 𝑢〉 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
| 70 | 66, 67, 69 | 3bitr3i 301 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉))) |
| 71 | 70 | imbi1i 349 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ (((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) → 𝜃)) |
| 72 | | impexp 450 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ 〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
| 73 | 71, 72 | bitri 275 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
| 74 | 73 | 3albii 1821 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃))) |
| 75 | 45, 65, 74 | 3bitr4ri 304 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
| 76 | | df-ral 3062 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑞 ∈
((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
| 77 | 75, 76 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃))) |
| 78 | | df-ral 3062 |
. . . . . . . . . . . . . 14
⊢
(∀𝑞 ∈
Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → [(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
| 79 | 44, 77, 78 | 3bitr4ri 304 |
. . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃)) |
| 80 | | frpoins3xp3g.1 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑤∀𝑡∀𝑢(〈𝑤, 𝑡, 𝑢〉 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉) → 𝜃) → 𝜑)) |
| 81 | 79, 80 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → 𝜑)) |
| 82 | | predeq3 6325 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)) |
| 83 | 82 | raleqdv 3326 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 〈𝑥, 𝑦, 𝑧〉)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃)) |
| 84 | | sbcoteq1a 8076 |
. . . . . . . . . . . . 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 247 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑))) |
| 87 | 86 | 3expia 1122 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐶 → (𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)))) |
| 88 | 25, 32, 87 | rexlimd 3266 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑))) |
| 89 | 88 | ex 412 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)))) |
| 90 | 19, 24, 89 | rexlimd 3266 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑))) |
| 91 | 18, 90 | rexlimi 3259 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = 〈𝑥, 𝑦, 𝑧〉 → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)) |
| 92 | 15, 91 | sylbi 217 |
. . . . 5
⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑤][(2nd
‘(1st ‘𝑞)) / 𝑡][(2nd ‘𝑞) / 𝑢]𝜃 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)) |
| 93 | 14, 92 | biimtrid 242 |
. . . 4
⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st
‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑 → [(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑)) |
| 94 | | 2fveq3 6911 |
. . . . 5
⊢ (𝑝 = 𝑞 → (1st
‘(1st ‘𝑝)) = (1st ‘(1st
‘𝑞))) |
| 95 | | 2fveq3 6911 |
. . . . . 6
⊢ (𝑝 = 𝑞 → (2nd
‘(1st ‘𝑝)) = (2nd ‘(1st
‘𝑞))) |
| 96 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → (2nd ‘𝑝) = (2nd ‘𝑞)) |
| 97 | 96 | sbceq1d 3793 |
. . . . . 6
⊢ (𝑝 = 𝑞 → ([(2nd ‘𝑝) / 𝑧]𝜑 ↔ [(2nd ‘𝑞) / 𝑧]𝜑)) |
| 98 | 95, 97 | sbceqbid 3795 |
. . . . 5
⊢ (𝑝 = 𝑞 → ([(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 ↔ [(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑)) |
| 99 | 94, 98 | sbceqbid 3795 |
. . . 4
⊢ (𝑝 = 𝑞 → ([(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 ↔ [(1st
‘(1st ‘𝑞)) / 𝑥][(2nd
‘(1st ‘𝑞)) / 𝑦][(2nd ‘𝑞) / 𝑧]𝜑)) |
| 100 | 93, 99 | frpoins2g 6366 |
. . 3
⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑) |
| 101 | | ralxp3es 8164 |
. . 3
⊢
(∀𝑝 ∈
((𝐴 × 𝐵) × 𝐶)[(1st
‘(1st ‘𝑝)) / 𝑥][(2nd
‘(1st ‘𝑝)) / 𝑦][(2nd ‘𝑝) / 𝑧]𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑) |
| 102 | 100, 101 | sylib 218 |
. 2
⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑) |
| 103 | | frpoins3xp3g.5 |
. . 3
⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜏)) |
| 104 | | frpoins3xp3g.6 |
. . 3
⊢ (𝑦 = 𝑌 → (𝜏 ↔ 𝜂)) |
| 105 | | frpoins3xp3g.7 |
. . 3
⊢ (𝑧 = 𝑍 → (𝜂 ↔ 𝜁)) |
| 106 | 103, 104,
105 | rspc3v 3638 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → 𝜁)) |
| 107 | 102, 106 | mpan9 506 |
1
⊢ (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜁) |