Step | Hyp | Ref
| Expression |
1 | | eqtr2 2819 |
. . . . . . . 8
⊢ ((𝑥 = ((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) ∧ 𝑥 = ((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟))) →
((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) =
((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟))) |
2 | | fvex 6658 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝑢) ∈ V |
3 | | fvex 6658 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝑣) ∈ V |
4 | | gonafv 32707 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝑢) ∈ V ∧ (1^{st} ‘𝑣) ∈ V) →
((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) =
⟨1_{o}, ⟨(1^{st} ‘𝑢), (1^{st} ‘𝑣)⟩⟩) |
5 | 2, 3, 4 | mp2an 691 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) =
⟨1_{o}, ⟨(1^{st} ‘𝑢), (1^{st} ‘𝑣)⟩⟩ |
6 | | fvex 6658 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝑠) ∈ V |
7 | | fvex 6658 |
. . . . . . . . . . . 12
⊢
(1^{st} ‘𝑟) ∈ V |
8 | | gonafv 32707 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝑠) ∈ V ∧ (1^{st} ‘𝑟) ∈ V) →
((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) =
⟨1_{o}, ⟨(1^{st} ‘𝑠), (1^{st} ‘𝑟)⟩⟩) |
9 | 6, 7, 8 | mp2an 691 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) =
⟨1_{o}, ⟨(1^{st} ‘𝑠), (1^{st} ‘𝑟)⟩⟩ |
10 | 5, 9 | eqeq12i 2813 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) =
((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) ↔
⟨1_{o}, ⟨(1^{st} ‘𝑢), (1^{st} ‘𝑣)⟩⟩ = ⟨1_{o},
⟨(1^{st} ‘𝑠), (1^{st} ‘𝑟)⟩⟩) |
11 | | 1oex 8093 |
. . . . . . . . . . 11
⊢
1_{o} ∈ V |
12 | | opex 5321 |
. . . . . . . . . . 11
⊢
⟨(1^{st} ‘𝑢), (1^{st} ‘𝑣)⟩ ∈ V |
13 | 11, 12 | opth 5333 |
. . . . . . . . . 10
⊢
(⟨1_{o}, ⟨(1^{st} ‘𝑢), (1^{st} ‘𝑣)⟩⟩ = ⟨1_{o},
⟨(1^{st} ‘𝑠), (1^{st} ‘𝑟)⟩⟩ ↔ (1_{o} =
1_{o} ∧ ⟨(1^{st} ‘𝑢), (1^{st} ‘𝑣)⟩ = ⟨(1^{st} ‘𝑠), (1^{st} ‘𝑟)⟩)) |
14 | 2, 3 | opth 5333 |
. . . . . . . . . . 11
⊢
(⟨(1^{st} ‘𝑢), (1^{st} ‘𝑣)⟩ = ⟨(1^{st} ‘𝑠), (1^{st} ‘𝑟)⟩ ↔ ((1^{st}
‘𝑢) = (1^{st}
‘𝑠) ∧
(1^{st} ‘𝑣) =
(1^{st} ‘𝑟))) |
15 | 14 | anbi2i 625 |
. . . . . . . . . 10
⊢
((1_{o} = 1_{o} ∧ ⟨(1^{st} ‘𝑢), (1^{st} ‘𝑣)⟩ = ⟨(1^{st}
‘𝑠), (1^{st}
‘𝑟)⟩) ↔
(1_{o} = 1_{o} ∧ ((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)))) |
16 | 10, 13, 15 | 3bitri 300 |
. . . . . . . . 9
⊢
(((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) =
((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) ↔
(1_{o} = 1_{o} ∧ ((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)))) |
17 | | funfv1st2nd 7727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑍 ∧ 𝑠 ∈ 𝑍) → (𝑍‘(1^{st} ‘𝑠)) = (2^{nd}
‘𝑠)) |
18 | 17 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝑍 → (𝑠 ∈ 𝑍 → (𝑍‘(1^{st} ‘𝑠)) = (2^{nd}
‘𝑠))) |
19 | | funfv1st2nd 7727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑍 ∧ 𝑟 ∈ 𝑍) → (𝑍‘(1^{st} ‘𝑟)) = (2^{nd}
‘𝑟)) |
20 | 19 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝑍 → (𝑟 ∈ 𝑍 → (𝑍‘(1^{st} ‘𝑟)) = (2^{nd}
‘𝑟))) |
21 | 18, 20 | anim12d 611 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑍‘(1^{st} ‘𝑠)) = (2^{nd}
‘𝑠) ∧ (𝑍‘(1^{st}
‘𝑟)) =
(2^{nd} ‘𝑟)))) |
22 | | funfv1st2nd 7727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑍 ∧ 𝑢 ∈ 𝑍) → (𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑢)) |
23 | 22 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝑍 → (𝑢 ∈ 𝑍 → (𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑢))) |
24 | | funfv1st2nd 7727 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑍 ∧ 𝑣 ∈ 𝑍) → (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑣)) |
25 | 24 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝑍 → (𝑣 ∈ 𝑍 → (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑣))) |
26 | 23, 25 | anim12d 611 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑍 → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → ((𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑢) ∧ (𝑍‘(1^{st}
‘𝑣)) =
(2^{nd} ‘𝑣)))) |
27 | | fveq2 6645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1^{st} ‘𝑠) = (1^{st} ‘𝑢) → (𝑍‘(1^{st} ‘𝑠)) = (𝑍‘(1^{st} ‘𝑢))) |
28 | 27 | eqcoms 2806 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1^{st} ‘𝑢) = (1^{st} ‘𝑠) → (𝑍‘(1^{st} ‘𝑠)) = (𝑍‘(1^{st} ‘𝑢))) |
29 | 28 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → (𝑍‘(1^{st} ‘𝑠)) = (𝑍‘(1^{st} ‘𝑢))) |
30 | 29 | eqeq1d 2800 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → ((𝑍‘(1^{st} ‘𝑠)) = (2^{nd}
‘𝑠) ↔ (𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑠))) |
31 | | fveq2 6645 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1^{st} ‘𝑟) = (1^{st} ‘𝑣) → (𝑍‘(1^{st} ‘𝑟)) = (𝑍‘(1^{st} ‘𝑣))) |
32 | 31 | eqcoms 2806 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1^{st} ‘𝑣) = (1^{st} ‘𝑟) → (𝑍‘(1^{st} ‘𝑟)) = (𝑍‘(1^{st} ‘𝑣))) |
33 | 32 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → (𝑍‘(1^{st} ‘𝑟)) = (𝑍‘(1^{st} ‘𝑣))) |
34 | 33 | eqeq1d 2800 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → ((𝑍‘(1^{st} ‘𝑟)) = (2^{nd}
‘𝑟) ↔ (𝑍‘(1^{st}
‘𝑣)) =
(2^{nd} ‘𝑟))) |
35 | 30, 34 | anbi12d 633 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → (((𝑍‘(1^{st} ‘𝑠)) = (2^{nd}
‘𝑠) ∧ (𝑍‘(1^{st}
‘𝑟)) =
(2^{nd} ‘𝑟))
↔ ((𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑠) ∧ (𝑍‘(1^{st}
‘𝑣)) =
(2^{nd} ‘𝑟)))) |
36 | 35 | anbi1d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → ((((𝑍‘(1^{st} ‘𝑠)) = (2^{nd}
‘𝑠) ∧ (𝑍‘(1^{st}
‘𝑟)) =
(2^{nd} ‘𝑟))
∧ ((𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑢) ∧ (𝑍‘(1^{st}
‘𝑣)) =
(2^{nd} ‘𝑣)))
↔ (((𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑠) ∧ (𝑍‘(1^{st}
‘𝑣)) =
(2^{nd} ‘𝑟))
∧ ((𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑢) ∧ (𝑍‘(1^{st}
‘𝑣)) =
(2^{nd} ‘𝑣))))) |
37 | | eqtr2 2819 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑠)
∧ (𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑢)) →
(2^{nd} ‘𝑠) =
(2^{nd} ‘𝑢)) |
38 | 37 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑠)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑟)) ∧ ((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑢)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑣))) →
(2^{nd} ‘𝑠) =
(2^{nd} ‘𝑢)) |
39 | | eqtr2 2819 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑍‘(1^{st}
‘𝑣)) =
(2^{nd} ‘𝑟)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑣)) →
(2^{nd} ‘𝑟) =
(2^{nd} ‘𝑣)) |
40 | 39 | ad2ant2l 745 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑠)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑟)) ∧ ((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑢)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑣))) →
(2^{nd} ‘𝑟) =
(2^{nd} ‘𝑣)) |
41 | 38, 40 | ineq12d 4140 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑠)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑟)) ∧ ((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑢)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑣))) →
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟)) = ((2^{nd} ‘𝑢) ∩ (2^{nd}
‘𝑣))) |
42 | 36, 41 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → ((((𝑍‘(1^{st} ‘𝑠)) = (2^{nd}
‘𝑠) ∧ (𝑍‘(1^{st}
‘𝑟)) =
(2^{nd} ‘𝑟))
∧ ((𝑍‘(1^{st} ‘𝑢)) = (2^{nd}
‘𝑢) ∧ (𝑍‘(1^{st}
‘𝑣)) =
(2^{nd} ‘𝑣)))
→ ((2^{nd} ‘𝑠) ∩ (2^{nd} ‘𝑟)) = ((2^{nd}
‘𝑢) ∩
(2^{nd} ‘𝑣)))) |
43 | 42 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑍‘(1^{st}
‘𝑠)) =
(2^{nd} ‘𝑠)
∧ (𝑍‘(1^{st} ‘𝑟)) = (2^{nd}
‘𝑟)) ∧ ((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑢)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑣))) →
(((1^{st} ‘𝑢)
= (1^{st} ‘𝑠)
∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → ((2^{nd} ‘𝑠) ∩ (2^{nd}
‘𝑟)) =
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣)))) |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑍 → ((((𝑍‘(1^{st}
‘𝑠)) =
(2^{nd} ‘𝑠)
∧ (𝑍‘(1^{st} ‘𝑟)) = (2^{nd}
‘𝑟)) ∧ ((𝑍‘(1^{st}
‘𝑢)) =
(2^{nd} ‘𝑢)
∧ (𝑍‘(1^{st} ‘𝑣)) = (2^{nd}
‘𝑣))) →
(((1^{st} ‘𝑢)
= (1^{st} ‘𝑠)
∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟)) → ((2^{nd} ‘𝑠) ∩ (2^{nd}
‘𝑟)) =
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))))) |
45 | 21, 26, 44 | syl2and 610 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑍 → (((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st}
‘𝑣) = (1^{st}
‘𝑟)) →
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟)) = ((2^{nd} ‘𝑢) ∩ (2^{nd}
‘𝑣))))) |
46 | 45 | expd 419 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → (((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st}
‘𝑣) = (1^{st}
‘𝑟)) →
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟)) = ((2^{nd} ‘𝑢) ∩ (2^{nd}
‘𝑣)))))) |
47 | 46 | 3imp1 1344 |
. . . . . . . . . . . . . 14
⊢ (((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st}
‘𝑣) = (1^{st}
‘𝑟))) →
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟)) = ((2^{nd} ‘𝑢) ∩ (2^{nd}
‘𝑣))) |
48 | 47 | difeq2d 4050 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st}
‘𝑣) = (1^{st}
‘𝑟))) → ((𝑀 ↑_{m} ω)
∖ ((2^{nd} ‘𝑠) ∩ (2^{nd} ‘𝑟))) = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣)))) |
49 | 48 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st}
‘𝑣) = (1^{st}
‘𝑟))) ∧ (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))))) → ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣)))) |
50 | | eqeq12 2812 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣)))) → (𝑦 = 𝑤 ↔ ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))))) |
51 | 50 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st}
‘𝑣) = (1^{st}
‘𝑟))) ∧ (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))))) → (𝑦 = 𝑤 ↔ ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))))) |
52 | 49, 51 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st}
‘𝑣) = (1^{st}
‘𝑟))) ∧ (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))))) → 𝑦 = 𝑤) |
53 | 52 | exp43 440 |
. . . . . . . . . 10
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st}
‘𝑣) = (1^{st}
‘𝑟)) → (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) → (𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))) → 𝑦 = 𝑤)))) |
54 | 53 | adantld 494 |
. . . . . . . . 9
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((1_{o} = 1_{o}
∧ ((1^{st} ‘𝑢) = (1^{st} ‘𝑠) ∧ (1^{st} ‘𝑣) = (1^{st} ‘𝑟))) → (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) → (𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))) → 𝑦 = 𝑤)))) |
55 | 16, 54 | syl5bi 245 |
. . . . . . . 8
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) =
((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) → (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) → (𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))) → 𝑦 = 𝑤)))) |
56 | 1, 55 | syl5 34 |
. . . . . . 7
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) ∧ 𝑥 = ((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟))) → (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) → (𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))) → 𝑦 = 𝑤)))) |
57 | 56 | expd 419 |
. . . . . 6
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) → (𝑥 = ((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) → (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) → (𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))) → 𝑦 = 𝑤))))) |
58 | 57 | com35 98 |
. . . . 5
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) → (𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))) → (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) → (𝑥 = ((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) → 𝑦 = 𝑤))))) |
59 | 58 | impd 414 |
. . . 4
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣)))) → (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) → (𝑥 = ((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) → 𝑦 = 𝑤)))) |
60 | 59 | com24 95 |
. . 3
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) → (𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟))) → ((𝑥 = ((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣)))) → 𝑦 = 𝑤)))) |
61 | 60 | impd 414 |
. 2
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟)))) → ((𝑥 = ((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣)))) → 𝑦 = 𝑤))) |
62 | 61 | 3imp 1108 |
1
⊢ (((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ (𝑥 = ((1^{st} ‘𝑠)⊼_{𝑔}(1^{st}
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑠)
∩ (2^{nd} ‘𝑟)))) ∧ (𝑥 = ((1^{st} ‘𝑢)⊼_{𝑔}(1^{st}
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑_{m} ω) ∖
((2^{nd} ‘𝑢)
∩ (2^{nd} ‘𝑣))))) → 𝑦 = 𝑤) |