Proof of Theorem satffunlem
| Step | Hyp | Ref
| Expression |
| 1 | | eqtr2 2761 |
. . . . . . . 8
⊢ ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟))) →
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
((1st ‘𝑠)⊼𝑔(1st
‘𝑟))) |
| 2 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑢) ∈ V |
| 3 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑣) ∈ V |
| 4 | | gonafv 35355 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑢) ∈ V ∧ (1st ‘𝑣) ∈ V) →
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉) |
| 5 | 2, 3, 4 | mp2an 692 |
. . . . . . . . . . 11
⊢
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉 |
| 6 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑠) ∈ V |
| 7 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑟) ∈ V |
| 8 | | gonafv 35355 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑠) ∈ V ∧ (1st ‘𝑟) ∈ V) →
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
〈1o, 〈(1st ‘𝑠), (1st ‘𝑟)〉〉) |
| 9 | 6, 7, 8 | mp2an 692 |
. . . . . . . . . . 11
⊢
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
〈1o, 〈(1st ‘𝑠), (1st ‘𝑟)〉〉 |
| 10 | 5, 9 | eqeq12i 2755 |
. . . . . . . . . 10
⊢
(((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ↔
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉 = 〈1o,
〈(1st ‘𝑠), (1st ‘𝑟)〉〉) |
| 11 | | 1oex 8516 |
. . . . . . . . . . 11
⊢
1o ∈ V |
| 12 | | opex 5469 |
. . . . . . . . . . 11
⊢
〈(1st ‘𝑢), (1st ‘𝑣)〉 ∈ V |
| 13 | 11, 12 | opth 5481 |
. . . . . . . . . 10
⊢
(〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉 = 〈1o,
〈(1st ‘𝑠), (1st ‘𝑟)〉〉 ↔ (1o =
1o ∧ 〈(1st ‘𝑢), (1st ‘𝑣)〉 = 〈(1st ‘𝑠), (1st ‘𝑟)〉)) |
| 14 | 2, 3 | opth 5481 |
. . . . . . . . . . 11
⊢
(〈(1st ‘𝑢), (1st ‘𝑣)〉 = 〈(1st ‘𝑠), (1st ‘𝑟)〉 ↔ ((1st
‘𝑢) = (1st
‘𝑠) ∧
(1st ‘𝑣) =
(1st ‘𝑟))) |
| 15 | 14 | anbi2i 623 |
. . . . . . . . . 10
⊢
((1o = 1o ∧ 〈(1st ‘𝑢), (1st ‘𝑣)〉 = 〈(1st
‘𝑠), (1st
‘𝑟)〉) ↔
(1o = 1o ∧ ((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)))) |
| 16 | 10, 13, 15 | 3bitri 297 |
. . . . . . . . 9
⊢
(((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ↔
(1o = 1o ∧ ((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)))) |
| 17 | | funfv1st2nd 8071 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑍 ∧ 𝑠 ∈ 𝑍) → (𝑍‘(1st ‘𝑠)) = (2nd
‘𝑠)) |
| 18 | 17 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝑍 → (𝑠 ∈ 𝑍 → (𝑍‘(1st ‘𝑠)) = (2nd
‘𝑠))) |
| 19 | | funfv1st2nd 8071 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑍 ∧ 𝑟 ∈ 𝑍) → (𝑍‘(1st ‘𝑟)) = (2nd
‘𝑟)) |
| 20 | 19 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝑍 → (𝑟 ∈ 𝑍 → (𝑍‘(1st ‘𝑟)) = (2nd
‘𝑟))) |
| 21 | 18, 20 | anim12d 609 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑍‘(1st ‘𝑠)) = (2nd
‘𝑠) ∧ (𝑍‘(1st
‘𝑟)) =
(2nd ‘𝑟)))) |
| 22 | | funfv1st2nd 8071 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑍 ∧ 𝑢 ∈ 𝑍) → (𝑍‘(1st ‘𝑢)) = (2nd
‘𝑢)) |
| 23 | 22 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝑍 → (𝑢 ∈ 𝑍 → (𝑍‘(1st ‘𝑢)) = (2nd
‘𝑢))) |
| 24 | | funfv1st2nd 8071 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝑍 ∧ 𝑣 ∈ 𝑍) → (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑣)) |
| 25 | 24 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝑍 → (𝑣 ∈ 𝑍 → (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑣))) |
| 26 | 23, 25 | anim12d 609 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑍 → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → ((𝑍‘(1st ‘𝑢)) = (2nd
‘𝑢) ∧ (𝑍‘(1st
‘𝑣)) =
(2nd ‘𝑣)))) |
| 27 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1st ‘𝑠) = (1st ‘𝑢) → (𝑍‘(1st ‘𝑠)) = (𝑍‘(1st ‘𝑢))) |
| 28 | 27 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑢) = (1st ‘𝑠) → (𝑍‘(1st ‘𝑠)) = (𝑍‘(1st ‘𝑢))) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)) → (𝑍‘(1st ‘𝑠)) = (𝑍‘(1st ‘𝑢))) |
| 30 | 29 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)) → ((𝑍‘(1st ‘𝑠)) = (2nd
‘𝑠) ↔ (𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑠))) |
| 31 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1st ‘𝑟) = (1st ‘𝑣) → (𝑍‘(1st ‘𝑟)) = (𝑍‘(1st ‘𝑣))) |
| 32 | 31 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((1st ‘𝑣) = (1st ‘𝑟) → (𝑍‘(1st ‘𝑟)) = (𝑍‘(1st ‘𝑣))) |
| 33 | 32 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)) → (𝑍‘(1st ‘𝑟)) = (𝑍‘(1st ‘𝑣))) |
| 34 | 33 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)) → ((𝑍‘(1st ‘𝑟)) = (2nd
‘𝑟) ↔ (𝑍‘(1st
‘𝑣)) =
(2nd ‘𝑟))) |
| 35 | 30, 34 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)) → (((𝑍‘(1st ‘𝑠)) = (2nd
‘𝑠) ∧ (𝑍‘(1st
‘𝑟)) =
(2nd ‘𝑟))
↔ ((𝑍‘(1st ‘𝑢)) = (2nd
‘𝑠) ∧ (𝑍‘(1st
‘𝑣)) =
(2nd ‘𝑟)))) |
| 36 | 35 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)) → ((((𝑍‘(1st ‘𝑠)) = (2nd
‘𝑠) ∧ (𝑍‘(1st
‘𝑟)) =
(2nd ‘𝑟))
∧ ((𝑍‘(1st ‘𝑢)) = (2nd
‘𝑢) ∧ (𝑍‘(1st
‘𝑣)) =
(2nd ‘𝑣)))
↔ (((𝑍‘(1st ‘𝑢)) = (2nd
‘𝑠) ∧ (𝑍‘(1st
‘𝑣)) =
(2nd ‘𝑟))
∧ ((𝑍‘(1st ‘𝑢)) = (2nd
‘𝑢) ∧ (𝑍‘(1st
‘𝑣)) =
(2nd ‘𝑣))))) |
| 37 | | eqtr2 2761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑠)
∧ (𝑍‘(1st ‘𝑢)) = (2nd
‘𝑢)) →
(2nd ‘𝑠) =
(2nd ‘𝑢)) |
| 38 | 37 | ad2ant2r 747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑠)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑟)) ∧ ((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑢)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑣))) →
(2nd ‘𝑠) =
(2nd ‘𝑢)) |
| 39 | | eqtr2 2761 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑍‘(1st
‘𝑣)) =
(2nd ‘𝑟)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑣)) →
(2nd ‘𝑟) =
(2nd ‘𝑣)) |
| 40 | 39 | ad2ant2l 746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑠)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑟)) ∧ ((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑢)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑣))) →
(2nd ‘𝑟) =
(2nd ‘𝑣)) |
| 41 | 38, 40 | ineq12d 4221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑠)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑟)) ∧ ((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑢)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑣))) →
((2nd ‘𝑠)
∩ (2nd ‘𝑟)) = ((2nd ‘𝑢) ∩ (2nd
‘𝑣))) |
| 42 | 36, 41 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟)) → ((((𝑍‘(1st ‘𝑠)) = (2nd
‘𝑠) ∧ (𝑍‘(1st
‘𝑟)) =
(2nd ‘𝑟))
∧ ((𝑍‘(1st ‘𝑢)) = (2nd
‘𝑢) ∧ (𝑍‘(1st
‘𝑣)) =
(2nd ‘𝑣)))
→ ((2nd ‘𝑠) ∩ (2nd ‘𝑟)) = ((2nd
‘𝑢) ∩
(2nd ‘𝑣)))) |
| 43 | 42 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑍‘(1st
‘𝑠)) =
(2nd ‘𝑠)
∧ (𝑍‘(1st ‘𝑟)) = (2nd
‘𝑟)) ∧ ((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑢)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑣))) →
(((1st ‘𝑢)
= (1st ‘𝑠)
∧ (1st ‘𝑣) = (1st ‘𝑟)) → ((2nd ‘𝑠) ∩ (2nd
‘𝑟)) =
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) |
| 44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝑍 → ((((𝑍‘(1st
‘𝑠)) =
(2nd ‘𝑠)
∧ (𝑍‘(1st ‘𝑟)) = (2nd
‘𝑟)) ∧ ((𝑍‘(1st
‘𝑢)) =
(2nd ‘𝑢)
∧ (𝑍‘(1st ‘𝑣)) = (2nd
‘𝑣))) →
(((1st ‘𝑢)
= (1st ‘𝑠)
∧ (1st ‘𝑣) = (1st ‘𝑟)) → ((2nd ‘𝑠) ∩ (2nd
‘𝑟)) =
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) |
| 45 | 21, 26, 44 | syl2and 608 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑍 → (((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st
‘𝑣) = (1st
‘𝑟)) →
((2nd ‘𝑠)
∩ (2nd ‘𝑟)) = ((2nd ‘𝑢) ∩ (2nd
‘𝑣))))) |
| 46 | 45 | expd 415 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝑍 → ((𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) → ((𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍) → (((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st
‘𝑣) = (1st
‘𝑟)) →
((2nd ‘𝑠)
∩ (2nd ‘𝑟)) = ((2nd ‘𝑢) ∩ (2nd
‘𝑣)))))) |
| 47 | 46 | 3imp1 1348 |
. . . . . . . . . . . . . 14
⊢ (((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st
‘𝑣) = (1st
‘𝑟))) →
((2nd ‘𝑠)
∩ (2nd ‘𝑟)) = ((2nd ‘𝑢) ∩ (2nd
‘𝑣))) |
| 48 | 47 | difeq2d 4126 |
. . . . . . . . . . . . 13
⊢ (((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st
‘𝑣) = (1st
‘𝑟))) → ((𝑀 ↑m ω)
∖ ((2nd ‘𝑠) ∩ (2nd ‘𝑟))) = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st
‘𝑣) = (1st
‘𝑟))) ∧ (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) → ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) |
| 50 | | eqeq12 2754 |
. . . . . . . . . . . . 13
⊢ ((𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → (𝑦 = 𝑤 ↔ ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st
‘𝑣) = (1st
‘𝑟))) ∧ (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) → (𝑦 = 𝑤 ↔ ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) |
| 52 | 49, 51 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ ((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st
‘𝑣) = (1st
‘𝑟))) ∧ (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) → 𝑦 = 𝑤) |
| 53 | 52 | exp43 436 |
. . . . . . . . . 10
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st
‘𝑣) = (1st
‘𝑟)) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → (𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) → 𝑦 = 𝑤)))) |
| 54 | 53 | adantld 490 |
. . . . . . . . 9
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((1o = 1o
∧ ((1st ‘𝑢) = (1st ‘𝑠) ∧ (1st ‘𝑣) = (1st ‘𝑟))) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → (𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) → 𝑦 = 𝑤)))) |
| 55 | 16, 54 | biimtrid 242 |
. . . . . . . 8
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → (𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) → 𝑦 = 𝑤)))) |
| 56 | 1, 55 | syl5 34 |
. . . . . . 7
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟))) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → (𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) → 𝑦 = 𝑤)))) |
| 57 | 56 | expd 415 |
. . . . . 6
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → (𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) → 𝑦 = 𝑤))))) |
| 58 | 57 | com35 98 |
. . . . 5
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → (𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → 𝑦 = 𝑤))))) |
| 59 | 58 | impd 410 |
. . . 4
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → 𝑦 = 𝑤)))) |
| 60 | 59 | com24 95 |
. . 3
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → 𝑦 = 𝑤)))) |
| 61 | 60 | impd 410 |
. 2
⊢ ((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → 𝑦 = 𝑤))) |
| 62 | 61 | 3imp 1111 |
1
⊢ (((Fun
𝑍 ∧ (𝑠 ∈ 𝑍 ∧ 𝑟 ∈ 𝑍) ∧ (𝑢 ∈ 𝑍 ∧ 𝑣 ∈ 𝑍)) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) → 𝑦 = 𝑤) |