Proof of Theorem psgnunilem1
Step | Hyp | Ref
| Expression |
1 | | psgnunilem1.q |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ∈ 𝑇) |
2 | | eqid 2622 |
. . . . . . . . 9
⊢
(pmTrsp‘𝐷) =
(pmTrsp‘𝐷) |
3 | | psgnunilem1.t |
. . . . . . . . 9
⊢ 𝑇 = ran (pmTrsp‘𝐷) |
4 | 2, 3 | pmtrfinv 17881 |
. . . . . . . 8
⊢ (𝑄 ∈ 𝑇 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷)) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑄 ∘ 𝑄) = ( I ↾ 𝐷)) |
6 | | coeq1 5279 |
. . . . . . . 8
⊢ (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑄)) |
7 | 6 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑃 = 𝑄 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ↔ (𝑄 ∘ 𝑄) = ( I ↾ 𝐷))) |
8 | 5, 7 | syl5ibrcom 237 |
. . . . . 6
⊢ (𝜑 → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷))) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 = 𝑄 → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷))) |
10 | 9 | imp 445 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → (𝑃 ∘ 𝑄) = ( I ↾ 𝐷)) |
11 | 10 | orcd 407 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 = 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) |
12 | | psgnunilem1.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ 𝑇) |
13 | 2, 3 | pmtrfcnv 17884 |
. . . . . . . . . 10
⊢ (𝑃 ∈ 𝑇 → ◡𝑃 = 𝑃) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ◡𝑃 = 𝑃) |
15 | 14 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 = ◡𝑃) |
16 | 15 | coeq2d 5284 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ ◡𝑃)) |
17 | 2, 3 | pmtrff1o 17883 |
. . . . . . . . 9
⊢ (𝑃 ∈ 𝑇 → 𝑃:𝐷–1-1-onto→𝐷) |
18 | 12, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃:𝐷–1-1-onto→𝐷) |
19 | 2, 3 | pmtrfconj 17886 |
. . . . . . . 8
⊢ ((𝑄 ∈ 𝑇 ∧ 𝑃:𝐷–1-1-onto→𝐷) → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇) |
20 | 1, 18, 19 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∈ 𝑇) |
21 | 16, 20 | eqeltrd 2701 |
. . . . . 6
⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇) |
22 | 21 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇) |
23 | 12 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝑃 ∈ 𝑇) |
24 | | coass 5654 |
. . . . . . 7
⊢ (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) = ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) |
25 | 2, 3 | pmtrfinv 17881 |
. . . . . . . . . 10
⊢ (𝑃 ∈ 𝑇 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷)) |
26 | 12, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 ∘ 𝑃) = ( I ↾ 𝐷)) |
27 | 26 | coeq2d 5284 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷))) |
28 | | f1of 6137 |
. . . . . . . . . . 11
⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃:𝐷⟶𝐷) |
29 | 18, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃:𝐷⟶𝐷) |
30 | 2, 3 | pmtrff1o 17883 |
. . . . . . . . . . . 12
⊢ (𝑄 ∈ 𝑇 → 𝑄:𝐷–1-1-onto→𝐷) |
31 | 1, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄:𝐷–1-1-onto→𝐷) |
32 | | f1of 6137 |
. . . . . . . . . . 11
⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄:𝐷⟶𝐷) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄:𝐷⟶𝐷) |
34 | | fco 6058 |
. . . . . . . . . 10
⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷⟶𝐷) → (𝑃 ∘ 𝑄):𝐷⟶𝐷) |
35 | 29, 33, 34 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 ∘ 𝑄):𝐷⟶𝐷) |
36 | | fcoi1 6078 |
. . . . . . . . 9
⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄)) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ ( I ↾ 𝐷)) = (𝑃 ∘ 𝑄)) |
38 | 27, 37 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ∘ 𝑄) ∘ (𝑃 ∘ 𝑃)) = (𝑃 ∘ 𝑄)) |
39 | 24, 38 | syl5req 2669 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃)) |
40 | 39 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃)) |
41 | | psgnunilem1.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom (𝑃 ∖ I )) |
42 | 41 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → 𝐴 ∈ dom (𝑃 ∖ I )) |
43 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃:𝐷–1-1-onto→𝐷) |
44 | 31 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑄:𝐷–1-1-onto→𝐷) |
45 | 2, 3 | pmtrfb 17885 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑃:𝐷–1-1-onto→𝐷 ∧ dom (𝑃 ∖ I ) ≈
2𝑜)) |
46 | 45 | simp3bi 1078 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ 𝑇 → dom (𝑃 ∖ I ) ≈
2𝑜) |
47 | 12, 46 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑃 ∖ I ) ≈
2𝑜) |
48 | 47 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈
2𝑜) |
49 | | 2onn 7720 |
. . . . . . . . . . . . . . 15
⊢
2𝑜 ∈ ω |
50 | | nnfi 8153 |
. . . . . . . . . . . . . . 15
⊢
(2𝑜 ∈ ω → 2𝑜
∈ Fin) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
2𝑜 ∈ Fin |
52 | 2, 3 | pmtrfb 17885 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑄 ∈ 𝑇 ↔ (𝐷 ∈ V ∧ 𝑄:𝐷–1-1-onto→𝐷 ∧ dom (𝑄 ∖ I ) ≈
2𝑜)) |
53 | 52 | simp3bi 1078 |
. . . . . . . . . . . . . . . 16
⊢ (𝑄 ∈ 𝑇 → dom (𝑄 ∖ I ) ≈
2𝑜) |
54 | 1, 53 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom (𝑄 ∖ I ) ≈
2𝑜) |
55 | | enfi 8176 |
. . . . . . . . . . . . . . 15
⊢ (dom
(𝑄 ∖ I ) ≈
2𝑜 → (dom (𝑄 ∖ I ) ∈ Fin ↔
2𝑜 ∈ Fin)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (dom (𝑄 ∖ I ) ∈ Fin ↔
2𝑜 ∈ Fin)) |
57 | 51, 56 | mpbiri 248 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝑄 ∖ I ) ∈ Fin) |
58 | 57 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) ∈
Fin) |
59 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑃 ∖ I )) |
60 | | en2eleq 8831 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom (𝑃 ∖ I ) ∧ dom (𝑃 ∖ I ) ≈ 2𝑜)
→ dom (𝑃 ∖ I ) =
{𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})}) |
61 | 59, 48, 60 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = {𝐴, ∪
(dom (𝑃 ∖ I ) ∖
{𝐴})}) |
62 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ dom (𝑄 ∖ I )) |
63 | | f1ofn 6138 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃:𝐷–1-1-onto→𝐷 → 𝑃 Fn 𝐷) |
64 | 18, 63 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 Fn 𝐷) |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 Fn 𝐷) |
66 | | imassrn 5477 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 “ dom (𝑄 ∖ I )) ⊆ ran 𝑃 |
67 | | frn 6053 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃:𝐷⟶𝐷 → ran 𝑃 ⊆ 𝐷) |
68 | 66, 67 | syl5ss 3614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃:𝐷⟶𝐷 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷) |
69 | 29, 68 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷) |
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷) |
71 | | simprr 796 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))) |
72 | | fnfvima 6496 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 Fn 𝐷 ∧ (𝑃 “ dom (𝑄 ∖ I )) ⊆ 𝐷 ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I )))) |
73 | 65, 70, 71, 72 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) ∈ (𝑃 “ (𝑃 “ dom (𝑄 ∖ I )))) |
74 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∖ I ) ⊆ 𝑃 |
75 | | dmss 5323 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∖ I ) ⊆ 𝑃 → dom (𝑃 ∖ I ) ⊆ dom 𝑃) |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ dom
(𝑃 ∖ I ) ⊆ dom
𝑃 |
77 | | f1odm 6141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:𝐷–1-1-onto→𝐷 → dom 𝑃 = 𝐷) |
78 | 18, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom 𝑃 = 𝐷) |
79 | 76, 78 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → dom (𝑃 ∖ I ) ⊆ 𝐷) |
80 | 79, 41 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈ 𝐷) |
81 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
(𝑃 ∖ I ) = dom (𝑃 ∖ I ) |
82 | 2, 3, 81 | pmtrffv 17879 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ 𝑇 ∧ 𝐴 ∈ 𝐷) → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪
(dom (𝑃 ∖ I ) ∖
{𝐴}), 𝐴)) |
83 | 12, 80, 82 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑃‘𝐴) = if(𝐴 ∈ dom (𝑃 ∖ I ), ∪
(dom (𝑃 ∖ I ) ∖
{𝐴}), 𝐴)) |
84 | 41 | iftrued 4094 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if(𝐴 ∈ dom (𝑃 ∖ I ), ∪
(dom (𝑃 ∖ I ) ∖
{𝐴}), 𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})) |
85 | 83, 84 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})) |
86 | 85 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃‘𝐴) = ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})) |
87 | | imaco 5640 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) |
88 | 26 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = (( I ↾ 𝐷) “ dom (𝑄 ∖ I ))) |
89 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑄 ∖ I ) ⊆ 𝑄 |
90 | | dmss 5323 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑄 ∖ I ) ⊆ 𝑄 → dom (𝑄 ∖ I ) ⊆ dom 𝑄) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ dom
(𝑄 ∖ I ) ⊆ dom
𝑄 |
92 | | f1odm 6141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom 𝑄 = 𝐷) |
93 | 91, 92 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑄:𝐷–1-1-onto→𝐷 → dom (𝑄 ∖ I ) ⊆ 𝐷) |
94 | 31, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → dom (𝑄 ∖ I ) ⊆ 𝐷) |
95 | | resiima 5480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (dom
(𝑄 ∖ I ) ⊆
𝐷 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I )) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (( I ↾ 𝐷) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I )) |
97 | 88, 96 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 ∘ 𝑃) “ dom (𝑄 ∖ I )) = dom (𝑄 ∖ I )) |
98 | 87, 97 | syl5eqr 2670 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I )) |
99 | 98 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → (𝑃 “ (𝑃 “ dom (𝑄 ∖ I ))) = dom (𝑄 ∖ I )) |
100 | 73, 86, 99 | 3eltr3d 2715 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}) ∈ dom (𝑄 ∖ I )) |
101 | | prssi 4353 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom (𝑄 ∖ I ) ∧ ∪ (dom (𝑃 ∖ I ) ∖ {𝐴}) ∈ dom (𝑄 ∖ I )) → {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})} ⊆ dom (𝑄 ∖ I )) |
102 | 62, 100, 101 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → {𝐴, ∪ (dom (𝑃 ∖ I ) ∖ {𝐴})} ⊆ dom (𝑄 ∖ I )) |
103 | 61, 102 | eqsstrd 3639 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ⊆ dom (𝑄 ∖ I )) |
104 | 54 | ensymd 8007 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2𝑜
≈ dom (𝑄 ∖ I
)) |
105 | | entr 8008 |
. . . . . . . . . . . . . 14
⊢ ((dom
(𝑃 ∖ I ) ≈
2𝑜 ∧ 2𝑜 ≈ dom (𝑄 ∖ I )) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I )) |
106 | 47, 104, 105 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I )) |
107 | 106 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) ≈ dom (𝑄 ∖ I )) |
108 | | fisseneq 8171 |
. . . . . . . . . . . 12
⊢ ((dom
(𝑄 ∖ I ) ∈ Fin
∧ dom (𝑃 ∖ I )
⊆ dom (𝑄 ∖ I )
∧ dom (𝑃 ∖ I )
≈ dom (𝑄 ∖ I ))
→ dom (𝑃 ∖ I ) =
dom (𝑄 ∖ I
)) |
109 | 58, 103, 107, 108 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑃 ∖ I ) = dom (𝑄 ∖ I )) |
110 | 109 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → dom (𝑄 ∖ I ) = dom (𝑃 ∖ I )) |
111 | | f1otrspeq 17867 |
. . . . . . . . . 10
⊢ (((𝑃:𝐷–1-1-onto→𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) ∧ (dom (𝑃 ∖ I ) ≈ 2𝑜
∧ dom (𝑄 ∖ I ) =
dom (𝑃 ∖ I ))) →
𝑃 = 𝑄) |
112 | 43, 44, 48, 110, 111 | syl22anc 1327 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴 ∈ dom (𝑄 ∖ I ) ∧ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) → 𝑃 = 𝑄) |
113 | 112 | expr 643 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )) → 𝑃 = 𝑄)) |
114 | 113 | necon3ad 2807 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ≠ 𝑄 → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) |
115 | 114 | imp 445 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I ))) |
116 | 16 | difeq1d 3727 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I )) |
117 | 116 | dmeqd 5326 |
. . . . . . . . 9
⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I )) |
118 | | f1omvdconj 17866 |
. . . . . . . . . 10
⊢ ((𝑄:𝐷⟶𝐷 ∧ 𝑃:𝐷–1-1-onto→𝐷) → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I ))) |
119 | 33, 18, 118 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ ◡𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I ))) |
120 | 117, 119 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜑 → dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) = (𝑃 “ dom (𝑄 ∖ I ))) |
121 | 120 | eleq2d 2687 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) |
122 | 121 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → (𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ) ↔ 𝐴 ∈ (𝑃 “ dom (𝑄 ∖ I )))) |
123 | 115, 122 | mtbird 315 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )) |
124 | | coeq1 5279 |
. . . . . . . 8
⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠)) |
125 | 124 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠))) |
126 | | difeq1 3721 |
. . . . . . . . . 10
⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝑟 ∖ I ) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )) |
127 | 126 | dmeqd 5326 |
. . . . . . . . 9
⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → dom (𝑟 ∖ I ) = dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )) |
128 | 127 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))) |
129 | 128 | notbid 308 |
. . . . . . 7
⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))) |
130 | 125, 129 | 3anbi13d 1401 |
. . . . . 6
⊢ (𝑟 = ((𝑃 ∘ 𝑄) ∘ 𝑃) → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))) |
131 | | coeq2 5280 |
. . . . . . . 8
⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃)) |
132 | 131 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑠 = 𝑃 → ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃))) |
133 | | difeq1 3721 |
. . . . . . . . 9
⊢ (𝑠 = 𝑃 → (𝑠 ∖ I ) = (𝑃 ∖ I )) |
134 | 133 | dmeqd 5326 |
. . . . . . . 8
⊢ (𝑠 = 𝑃 → dom (𝑠 ∖ I ) = dom (𝑃 ∖ I )) |
135 | 134 | eleq2d 2687 |
. . . . . . 7
⊢ (𝑠 = 𝑃 → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom (𝑃 ∖ I ))) |
136 | 132, 135 | 3anbi12d 1400 |
. . . . . 6
⊢ (𝑠 = 𝑃 → (((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I )))) |
137 | 130, 136 | rspc2ev 3324 |
. . . . 5
⊢ ((((𝑃 ∘ 𝑄) ∘ 𝑃) ∈ 𝑇 ∧ 𝑃 ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (((𝑃 ∘ 𝑄) ∘ 𝑃) ∘ 𝑃) ∧ 𝐴 ∈ dom (𝑃 ∖ I ) ∧ ¬ 𝐴 ∈ dom (((𝑃 ∘ 𝑄) ∘ 𝑃) ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))) |
138 | 22, 23, 40, 42, 123, 137 | syl113anc 1338 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))) |
139 | 138 | olcd 408 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) |
140 | 11, 139 | pm2.61dane 2881 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) |
141 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝑄 ∈ 𝑇) |
142 | | coass 5654 |
. . . . . . 7
⊢ ((𝑄 ∘ 𝑃) ∘ 𝑄) = (𝑄 ∘ (𝑃 ∘ 𝑄)) |
143 | 2, 3 | pmtrfcnv 17884 |
. . . . . . . . . 10
⊢ (𝑄 ∈ 𝑇 → ◡𝑄 = 𝑄) |
144 | 1, 143 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ◡𝑄 = 𝑄) |
145 | 144 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 = ◡𝑄) |
146 | 145 | coeq2d 5284 |
. . . . . . 7
⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ 𝑄) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄)) |
147 | 142, 146 | syl5eqr 2670 |
. . . . . 6
⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) = ((𝑄 ∘ 𝑃) ∘ ◡𝑄)) |
148 | 2, 3 | pmtrfconj 17886 |
. . . . . . 7
⊢ ((𝑃 ∈ 𝑇 ∧ 𝑄:𝐷–1-1-onto→𝐷) → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇) |
149 | 12, 31, 148 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∈ 𝑇) |
150 | 147, 149 | eqeltrd 2701 |
. . . . 5
⊢ (𝜑 → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇) |
151 | 150 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇) |
152 | 5 | coeq1d 5283 |
. . . . . . 7
⊢ (𝜑 → ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄))) |
153 | | fcoi2 6079 |
. . . . . . . 8
⊢ ((𝑃 ∘ 𝑄):𝐷⟶𝐷 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄)) |
154 | 35, 153 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (( I ↾ 𝐷) ∘ (𝑃 ∘ 𝑄)) = (𝑃 ∘ 𝑄)) |
155 | 152, 154 | eqtr2d 2657 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∘ 𝑄) = ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄))) |
156 | | coass 5654 |
. . . . . 6
⊢ ((𝑄 ∘ 𝑄) ∘ (𝑃 ∘ 𝑄)) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) |
157 | 155, 156 | syl6eq 2672 |
. . . . 5
⊢ (𝜑 → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))) |
158 | 157 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))) |
159 | | f1ofn 6138 |
. . . . . . . . . 10
⊢ (𝑄:𝐷–1-1-onto→𝐷 → 𝑄 Fn 𝐷) |
160 | 31, 159 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 Fn 𝐷) |
161 | | fnelnfp 6443 |
. . . . . . . . 9
⊢ ((𝑄 Fn 𝐷 ∧ 𝐴 ∈ 𝐷) → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴)) |
162 | 160, 80, 161 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ dom (𝑄 ∖ I ) ↔ (𝑄‘𝐴) ≠ 𝐴)) |
163 | 162 | necon2bbid 2837 |
. . . . . . 7
⊢ (𝜑 → ((𝑄‘𝐴) = 𝐴 ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))) |
164 | 163 | biimpar 502 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) = 𝐴) |
165 | | fnfvima 6496 |
. . . . . . . 8
⊢ ((𝑄 Fn 𝐷 ∧ dom (𝑃 ∖ I ) ⊆ 𝐷 ∧ 𝐴 ∈ dom (𝑃 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I ))) |
166 | 160, 79, 41, 165 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I ))) |
167 | 166 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → (𝑄‘𝐴) ∈ (𝑄 “ dom (𝑃 ∖ I ))) |
168 | 164, 167 | eqeltrrd 2702 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ (𝑄 “ dom (𝑃 ∖ I ))) |
169 | 147 | difeq1d 3727 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I )) |
170 | 169 | dmeqd 5326 |
. . . . . . 7
⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I )) |
171 | | f1omvdconj 17866 |
. . . . . . . 8
⊢ ((𝑃:𝐷⟶𝐷 ∧ 𝑄:𝐷–1-1-onto→𝐷) → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I ))) |
172 | 29, 31, 171 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → dom (((𝑄 ∘ 𝑃) ∘ ◡𝑄) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I ))) |
173 | 170, 172 | eqtrd 2656 |
. . . . . 6
⊢ (𝜑 → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I ))) |
174 | 173 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) = (𝑄 “ dom (𝑃 ∖ I ))) |
175 | 168, 174 | eleqtrrd 2704 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I )) |
176 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ¬ 𝐴 ∈ dom (𝑄 ∖ I )) |
177 | | coeq1 5279 |
. . . . . . 7
⊢ (𝑟 = 𝑄 → (𝑟 ∘ 𝑠) = (𝑄 ∘ 𝑠)) |
178 | 177 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑟 = 𝑄 → ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠))) |
179 | | difeq1 3721 |
. . . . . . . . 9
⊢ (𝑟 = 𝑄 → (𝑟 ∖ I ) = (𝑄 ∖ I )) |
180 | 179 | dmeqd 5326 |
. . . . . . . 8
⊢ (𝑟 = 𝑄 → dom (𝑟 ∖ I ) = dom (𝑄 ∖ I )) |
181 | 180 | eleq2d 2687 |
. . . . . . 7
⊢ (𝑟 = 𝑄 → (𝐴 ∈ dom (𝑟 ∖ I ) ↔ 𝐴 ∈ dom (𝑄 ∖ I ))) |
182 | 181 | notbid 308 |
. . . . . 6
⊢ (𝑟 = 𝑄 → (¬ 𝐴 ∈ dom (𝑟 ∖ I ) ↔ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))) |
183 | 178, 182 | 3anbi13d 1401 |
. . . . 5
⊢ (𝑟 = 𝑄 → (((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))) |
184 | | coeq2 5280 |
. . . . . . 7
⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑄 ∘ 𝑠) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄)))) |
185 | 184 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → ((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ↔ (𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))))) |
186 | | difeq1 3721 |
. . . . . . . 8
⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝑠 ∖ I ) = ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I )) |
187 | 186 | dmeqd 5326 |
. . . . . . 7
⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → dom (𝑠 ∖ I ) = dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I )) |
188 | 187 | eleq2d 2687 |
. . . . . 6
⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (𝐴 ∈ dom (𝑠 ∖ I ) ↔ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ))) |
189 | 185, 188 | 3anbi12d 1400 |
. . . . 5
⊢ (𝑠 = (𝑄 ∘ (𝑃 ∘ 𝑄)) → (((𝑃 ∘ 𝑄) = (𝑄 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) ↔ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )))) |
190 | 183, 189 | rspc2ev 3324 |
. . . 4
⊢ ((𝑄 ∈ 𝑇 ∧ (𝑄 ∘ (𝑃 ∘ 𝑄)) ∈ 𝑇 ∧ ((𝑃 ∘ 𝑄) = (𝑄 ∘ (𝑄 ∘ (𝑃 ∘ 𝑄))) ∧ 𝐴 ∈ dom ((𝑄 ∘ (𝑃 ∘ 𝑄)) ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I ))) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))) |
191 | 141, 151,
158, 175, 176, 190 | syl113anc 1338 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))) |
192 | 191 | olcd 408 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ dom (𝑄 ∖ I )) → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) |
193 | 140, 192 | pm2.61dan 832 |
1
⊢ (𝜑 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) |