Metamath Proof Explorer

Theorem f1omvdco3

Description: If a point is moved by exactly one of two permutations, then it will be moved by their composite. (Contributed by Stefan O'Rear, 23-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 notbi ⊢ ( ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) ↔ ( ¬ 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ ¬ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) )
2 disjsn ⊢ ( ( dom ( 𝐹 ∖ I ) ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ dom ( 𝐹 ∖ I ) )
3 disj2 ⊢ ( ( dom ( 𝐹 ∖ I ) ∩ { 𝑋 } ) = ∅ ↔ dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) )
4 2 3 bitr3i ⊢ ( ¬ 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) )
5 disjsn ⊢ ( ( dom ( 𝐺 ∖ I ) ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ dom ( 𝐺 ∖ I ) )
6 disj2 ⊢ ( ( dom ( 𝐺 ∖ I ) ∩ { 𝑋 } ) = ∅ ↔ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) )
7 5 6 bitr3i ⊢ ( ¬ 𝑋 ∈ dom ( 𝐺 ∖ I ) ↔ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) )
8 4 7 bibi12i ⊢ ( ( ¬ 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ ¬ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) ↔ ( dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ↔ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ) )
9 1 8 bitri ⊢ ( ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) ↔ ( dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ↔ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ) )
10 9 notbii ⊢ ( ¬ ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) ↔ ¬ ( dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ↔ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ) )
11 df-xor ⊢ ( ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ⊻ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) ↔ ¬ ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ↔ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) )
12 df-xor ⊢ ( ( dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ⊻ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ) ↔ ¬ ( dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ↔ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ) )
13 10 11 12 3bitr4i ⊢ ( ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ⊻ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) ↔ ( dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ⊻ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ) )
14 f1omvdco2 ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ∧ ( dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ⊻ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ) ) → ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ ( V ∖ { 𝑋 } ) )
15 disj2 ⊢ ( ( dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ∩ { 𝑋 } ) = ∅ ↔ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ ( V ∖ { 𝑋 } ) )
16 disjsn ⊢ ( ( dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) )
17 15 16 bitr3i ⊢ ( dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ↔ ¬ 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) )
18 17 con2bii ⊢ ( 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ↔ ¬ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) ⊆ ( V ∖ { 𝑋 } ) )
19 14 18 sylibr ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ∧ ( dom ( 𝐹 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ⊻ dom ( 𝐺 ∖ I ) ⊆ ( V ∖ { 𝑋 } ) ) ) → 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) )
20 13 19 syl3an3b ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ∧ ( 𝑋 ∈ dom ( 𝐹 ∖ I ) ⊻ 𝑋 ∈ dom ( 𝐺 ∖ I ) ) ) → 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ∖ I ) )