Metamath Proof Explorer

Theorem f1omvdco2

Description: If exactly one of two permutations is limited to a set of points, then the composition will not be. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion f1omvdco2 ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ⊻ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) ) → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 )

Proof

Step Hyp Ref Expression
1 excxor ⊢ ( ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ⊻ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) ↔ ( ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ ¬ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) ∨ ( ¬ dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) ) )
2 coass ⊢ ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) )
3 f1ococnv1 ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) )
4 3 coeq1d ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = ( ( I ↾ 𝐴 ) ∘ 𝐺 ) )
5 f1of ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐴 → 𝐺 : 𝐴 ⟶ 𝐴 )
6 fcoi2 ⊢ ( 𝐺 : 𝐴 ⟶ 𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝐺 ) = 𝐺 )
7 5 6 syl ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐴 → ( ( I ↾ 𝐴 ) ∘ 𝐺 ) = 𝐺 )
8 4 7 sylan9eq ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( ◡ 𝐹 ∘ 𝐹 ) ∘ 𝐺 ) = 𝐺 )
9 2 8 eqtr3id ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) = 𝐺 )
10 9 difeq1d ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ∖ I ) = ( 𝐺 ∖ I ) )
11 10 dmeqd ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → dom ( ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ∖ I ) = dom ( 𝐺 ∖ I ) )
12 11 adantr ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ∖ I ) = dom ( 𝐺 ∖ I ) )
13 mvdco ⊢ dom ( ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ∖ I ) ⊆ ( dom ( ◡ 𝐹 ∖ I ) ∪ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) )
14 f1omvdcnv ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → dom ( ◡ 𝐹 ∖ I ) = dom ( 𝐹 ∖ I ) )
15 14 ad2antrr ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ◡ 𝐹 ∖ I ) = dom ( 𝐹 ∖ I ) )
16 simprl ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( 𝐹 ∖ I ) ⊆ 𝑋 )
17 15 16 eqsstrd ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ◡ 𝐹 ∖ I ) ⊆ 𝑋 )
18 simprr ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 )
19 17 18 unssd ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → ( dom ( ◡ 𝐹 ∖ I ) ∪ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ) ⊆ 𝑋 )
20 13 19 sstrid ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ( ◡ 𝐹 ∘ ( 𝐹 ∘ 𝐺 ) ) ∖ I ) ⊆ 𝑋 )
21 12 20 eqsstrrd ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( 𝐺 ∖ I ) ⊆ 𝑋 )
22 21 expr ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ dom ( 𝐹 ∖ I ) ⊆ 𝑋 ) → ( dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 → dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) )
23 22 con3d ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ dom ( 𝐹 ∖ I ) ⊆ 𝑋 ) → ( ¬ dom ( 𝐺 ∖ I ) ⊆ 𝑋 → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) )
24 23 expimpd ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ ¬ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) )
25 coass ⊢ ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) = ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) )
26 f1ococnv2 ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐴 → ( 𝐺 ∘ ◡ 𝐺 ) = ( I ↾ 𝐴 ) )
27 26 coeq2d ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐴 → ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) ) = ( 𝐹 ∘ ( I ↾ 𝐴 ) ) )
28 f1of ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 : 𝐴 ⟶ 𝐴 )
29 fcoi1 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐴 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = 𝐹 )
30 28 29 syl ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → ( 𝐹 ∘ ( I ↾ 𝐴 ) ) = 𝐹 )
31 27 30 sylan9eqr ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( 𝐹 ∘ ( 𝐺 ∘ ◡ 𝐺 ) ) = 𝐹 )
32 25 31 eqtrid ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) = 𝐹 )
33 32 difeq1d ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) ∖ I ) = ( 𝐹 ∖ I ) )
34 33 dmeqd ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → dom ( ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) ∖ I ) = dom ( 𝐹 ∖ I ) )
35 34 adantr ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) ∖ I ) = dom ( 𝐹 ∖ I ) )
36 mvdco ⊢ dom ( ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) ∖ I ) ⊆ ( dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ∪ dom ( ◡ 𝐺 ∖ I ) )
37 simprr ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 )
38 f1omvdcnv ⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐴 → dom ( ◡ 𝐺 ∖ I ) = dom ( 𝐺 ∖ I ) )
39 38 ad2antlr ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ◡ 𝐺 ∖ I ) = dom ( 𝐺 ∖ I ) )
40 simprl ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( 𝐺 ∖ I ) ⊆ 𝑋 )
41 39 40 eqsstrd ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ◡ 𝐺 ∖ I ) ⊆ 𝑋 )
42 37 41 unssd ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → ( dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ∪ dom ( ◡ 𝐺 ∖ I ) ) ⊆ 𝑋 )
43 36 42 sstrid ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( ( ( 𝐹 ∘ 𝐺 ) ∘ ◡ 𝐺 ) ∖ I ) ⊆ 𝑋 )
44 35 43 eqsstrrd ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) ) → dom ( 𝐹 ∖ I ) ⊆ 𝑋 )
45 44 expr ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) → ( dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 → dom ( 𝐹 ∖ I ) ⊆ 𝑋 ) )
46 45 con3d ⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) → ( ¬ dom ( 𝐹 ∖ I ) ⊆ 𝑋 → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) )
47 46 expimpd ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( dom ( 𝐺 ∖ I ) ⊆ 𝑋 ∧ ¬ dom ( 𝐹 ∖ I ) ⊆ 𝑋 ) → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) )
48 47 ancomsd ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( ¬ dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) )
49 24 48 jaod ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ ¬ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) ∨ ( ¬ dom ( 𝐹 ∖ I ) ⊆ 𝑋 ∧ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) ) → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) )
50 1 49 biimtrid ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) → ( ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ⊻ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 ) )
51 50 3impia ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ∧ ( dom ( 𝐹 ∖ I ) ⊆ 𝑋 ⊻ dom ( 𝐺 ∖ I ) ⊆ 𝑋 ) ) → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ 𝑋 )