Step |
Hyp |
Ref |
Expression |
1 |
|
eqtr2 |
⊢ ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) ) → ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) ) |
2 |
|
fvex |
⊢ ( 1st ‘ 𝑢 ) ∈ V |
3 |
|
fvex |
⊢ ( 1st ‘ 𝑣 ) ∈ V |
4 |
|
gonafv |
⊢ ( ( ( 1st ‘ 𝑢 ) ∈ V ∧ ( 1st ‘ 𝑣 ) ∈ V ) → ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) = 〈 1o , 〈 ( 1st ‘ 𝑢 ) , ( 1st ‘ 𝑣 ) 〉 〉 ) |
5 |
2 3 4
|
mp2an |
⊢ ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) = 〈 1o , 〈 ( 1st ‘ 𝑢 ) , ( 1st ‘ 𝑣 ) 〉 〉 |
6 |
|
fvex |
⊢ ( 1st ‘ 𝑠 ) ∈ V |
7 |
|
fvex |
⊢ ( 1st ‘ 𝑟 ) ∈ V |
8 |
|
gonafv |
⊢ ( ( ( 1st ‘ 𝑠 ) ∈ V ∧ ( 1st ‘ 𝑟 ) ∈ V ) → ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) = 〈 1o , 〈 ( 1st ‘ 𝑠 ) , ( 1st ‘ 𝑟 ) 〉 〉 ) |
9 |
6 7 8
|
mp2an |
⊢ ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) = 〈 1o , 〈 ( 1st ‘ 𝑠 ) , ( 1st ‘ 𝑟 ) 〉 〉 |
10 |
5 9
|
eqeq12i |
⊢ ( ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) ↔ 〈 1o , 〈 ( 1st ‘ 𝑢 ) , ( 1st ‘ 𝑣 ) 〉 〉 = 〈 1o , 〈 ( 1st ‘ 𝑠 ) , ( 1st ‘ 𝑟 ) 〉 〉 ) |
11 |
|
1oex |
⊢ 1o ∈ V |
12 |
|
opex |
⊢ 〈 ( 1st ‘ 𝑢 ) , ( 1st ‘ 𝑣 ) 〉 ∈ V |
13 |
11 12
|
opth |
⊢ ( 〈 1o , 〈 ( 1st ‘ 𝑢 ) , ( 1st ‘ 𝑣 ) 〉 〉 = 〈 1o , 〈 ( 1st ‘ 𝑠 ) , ( 1st ‘ 𝑟 ) 〉 〉 ↔ ( 1o = 1o ∧ 〈 ( 1st ‘ 𝑢 ) , ( 1st ‘ 𝑣 ) 〉 = 〈 ( 1st ‘ 𝑠 ) , ( 1st ‘ 𝑟 ) 〉 ) ) |
14 |
2 3
|
opth |
⊢ ( 〈 ( 1st ‘ 𝑢 ) , ( 1st ‘ 𝑣 ) 〉 = 〈 ( 1st ‘ 𝑠 ) , ( 1st ‘ 𝑟 ) 〉 ↔ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) |
15 |
14
|
anbi2i |
⊢ ( ( 1o = 1o ∧ 〈 ( 1st ‘ 𝑢 ) , ( 1st ‘ 𝑣 ) 〉 = 〈 ( 1st ‘ 𝑠 ) , ( 1st ‘ 𝑟 ) 〉 ) ↔ ( 1o = 1o ∧ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) ) |
16 |
10 13 15
|
3bitri |
⊢ ( ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) ↔ ( 1o = 1o ∧ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) ) |
17 |
|
funfv1st2nd |
⊢ ( ( Fun 𝑍 ∧ 𝑠 ∈ 𝑍 ) → ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ) |
18 |
17
|
ex |
⊢ ( Fun 𝑍 → ( 𝑠 ∈ 𝑍 → ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ) ) |
19 |
|
funfv1st2nd |
⊢ ( ( Fun 𝑍 ∧ 𝑟 ∈ 𝑍 ) → ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ) |
20 |
19
|
ex |
⊢ ( Fun 𝑍 → ( 𝑟 ∈ 𝑍 → ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ) ) |
21 |
18 20
|
anim12d |
⊢ ( Fun 𝑍 → ( ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) → ( ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ) ) ) |
22 |
|
funfv1st2nd |
⊢ ( ( Fun 𝑍 ∧ 𝑢 ∈ 𝑍 ) → ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ) |
23 |
22
|
ex |
⊢ ( Fun 𝑍 → ( 𝑢 ∈ 𝑍 → ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ) ) |
24 |
|
funfv1st2nd |
⊢ ( ( Fun 𝑍 ∧ 𝑣 ∈ 𝑍 ) → ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) |
25 |
24
|
ex |
⊢ ( Fun 𝑍 → ( 𝑣 ∈ 𝑍 → ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) |
26 |
23 25
|
anim12d |
⊢ ( Fun 𝑍 → ( ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) → ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) ) |
27 |
|
fveq2 |
⊢ ( ( 1st ‘ 𝑠 ) = ( 1st ‘ 𝑢 ) → ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) ) |
28 |
27
|
eqcoms |
⊢ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) → ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) ) |
29 |
28
|
adantr |
⊢ ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) ) |
30 |
29
|
eqeq1d |
⊢ ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ↔ ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑠 ) ) ) |
31 |
|
fveq2 |
⊢ ( ( 1st ‘ 𝑟 ) = ( 1st ‘ 𝑣 ) → ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) ) |
32 |
31
|
eqcoms |
⊢ ( ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) → ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) ) |
33 |
32
|
adantl |
⊢ ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) ) |
34 |
33
|
eqeq1d |
⊢ ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ↔ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑟 ) ) ) |
35 |
30 34
|
anbi12d |
⊢ ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ) ↔ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑟 ) ) ) ) |
36 |
35
|
anbi1d |
⊢ ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( ( ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) ↔ ( ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) ) ) |
37 |
|
eqtr2 |
⊢ ( ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ) → ( 2nd ‘ 𝑠 ) = ( 2nd ‘ 𝑢 ) ) |
38 |
37
|
ad2ant2r |
⊢ ( ( ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) → ( 2nd ‘ 𝑠 ) = ( 2nd ‘ 𝑢 ) ) |
39 |
|
eqtr2 |
⊢ ( ( ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑟 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) → ( 2nd ‘ 𝑟 ) = ( 2nd ‘ 𝑣 ) ) |
40 |
39
|
ad2ant2l |
⊢ ( ( ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) → ( 2nd ‘ 𝑟 ) = ( 2nd ‘ 𝑣 ) ) |
41 |
38 40
|
ineq12d |
⊢ ( ( ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) → ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) = ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) |
42 |
36 41
|
syl6bi |
⊢ ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( ( ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) → ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) = ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) |
43 |
42
|
com12 |
⊢ ( ( ( ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) → ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) = ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) |
44 |
43
|
a1i |
⊢ ( Fun 𝑍 → ( ( ( ( 𝑍 ‘ ( 1st ‘ 𝑠 ) ) = ( 2nd ‘ 𝑠 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑟 ) ) = ( 2nd ‘ 𝑟 ) ) ∧ ( ( 𝑍 ‘ ( 1st ‘ 𝑢 ) ) = ( 2nd ‘ 𝑢 ) ∧ ( 𝑍 ‘ ( 1st ‘ 𝑣 ) ) = ( 2nd ‘ 𝑣 ) ) ) → ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) = ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) |
45 |
21 26 44
|
syl2and |
⊢ ( Fun 𝑍 → ( ( ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) = ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) |
46 |
45
|
expd |
⊢ ( Fun 𝑍 → ( ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) → ( ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) → ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) = ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) ) |
47 |
46
|
3imp1 |
⊢ ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) → ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) = ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) |
48 |
47
|
difeq2d |
⊢ ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) → ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) |
49 |
48
|
adantr |
⊢ ( ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) ∧ ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) → ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) |
50 |
|
eqeq12 |
⊢ ( ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) → ( 𝑦 = 𝑤 ↔ ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) |
51 |
50
|
adantl |
⊢ ( ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) ∧ ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) → ( 𝑦 = 𝑤 ↔ ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) |
52 |
49 51
|
mpbird |
⊢ ( ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) ∧ ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) → 𝑦 = 𝑤 ) |
53 |
52
|
exp43 |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) ) |
54 |
53
|
adantld |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 1o = 1o ∧ ( ( 1st ‘ 𝑢 ) = ( 1st ‘ 𝑠 ) ∧ ( 1st ‘ 𝑣 ) = ( 1st ‘ 𝑟 ) ) ) → ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) ) |
55 |
16 54
|
syl5bi |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) ) |
56 |
1 55
|
syl5 |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑥 = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) ) → ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) ) |
57 |
56
|
expd |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) → ( 𝑥 = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) → ( 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) → 𝑦 = 𝑤 ) ) ) ) ) |
58 |
57
|
com35 |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) → ( 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) → ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) → ( 𝑥 = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) → 𝑦 = 𝑤 ) ) ) ) ) |
59 |
58
|
impd |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) → ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) → ( 𝑥 = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) → 𝑦 = 𝑤 ) ) ) ) |
60 |
59
|
com24 |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( 𝑥 = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) → ( 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) → ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) → 𝑦 = 𝑤 ) ) ) ) |
61 |
60
|
impd |
⊢ ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) → ( ( 𝑥 = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) ) → ( ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) → 𝑦 = 𝑤 ) ) ) |
62 |
61
|
3imp |
⊢ ( ( ( Fun 𝑍 ∧ ( 𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍 ) ∧ ( 𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍 ) ) ∧ ( 𝑥 = ( ( 1st ‘ 𝑠 ) ⊼𝑔 ( 1st ‘ 𝑟 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑠 ) ∩ ( 2nd ‘ 𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑤 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ) → 𝑦 = 𝑤 ) |