Metamath Proof Explorer


Theorem satffunlem

Description: Lemma for satffunlem1lem1 and satffunlem2lem1 . (Contributed by AV, 27-Oct-2023)

Ref Expression
Assertion satffunlem ( ( ( Fun 𝑍 ∧ ( 𝑠𝑍𝑟𝑍 ) ∧ ( 𝑢𝑍𝑣𝑍 ) ) ∧ ( 𝑥 = ( ( 1st𝑠 ) ⊼𝑔 ( 1st𝑟 ) ) ∧ 𝑦 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑠 ) ∩ ( 2nd𝑟 ) ) ) ) ∧ ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∧ 𝑤 = ( ( 𝑀m ω ) ∖ ( ( 2nd𝑢 ) ∩ ( 2nd𝑣 ) ) ) ) ) → 𝑦 = 𝑤 )

Proof

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𝑣 ) ) ) ) ) → 𝑦 = 𝑤 )