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 ⊢ F : A ⟶ 1-1 onto A ∧ G : A ⟶ 1-1 onto A ∧ X ∈ dom ⁡ F ∖ I ⊻ X ∈ dom ⁡ G ∖ I → X ∈ dom ⁡ F ∘ G ∖ I

Proof

Step Hyp Ref Expression
1 notbi ⊢ X ∈ dom ⁡ F ∖ I ↔ X ∈ dom ⁡ G ∖ I ↔ ¬ X ∈ dom ⁡ F ∖ I ↔ ¬ X ∈ dom ⁡ G ∖ I
2 disjsn ⊢ dom ⁡ F ∖ I ∩ X = ∅ ↔ ¬ X ∈ dom ⁡ F ∖ I
3 disj2 ⊢ dom ⁡ F ∖ I ∩ X = ∅ ↔ dom ⁡ F ∖ I ⊆ V ∖ X
4 2 3 bitr3i ⊢ ¬ X ∈ dom ⁡ F ∖ I ↔ dom ⁡ F ∖ I ⊆ V ∖ X
5 disjsn ⊢ dom ⁡ G ∖ I ∩ X = ∅ ↔ ¬ X ∈ dom ⁡ G ∖ I
6 disj2 ⊢ dom ⁡ G ∖ I ∩ X = ∅ ↔ dom ⁡ G ∖ I ⊆ V ∖ X
7 5 6 bitr3i ⊢ ¬ X ∈ dom ⁡ G ∖ I ↔ dom ⁡ G ∖ I ⊆ V ∖ X
8 4 7 bibi12i ⊢ ¬ X ∈ dom ⁡ F ∖ I ↔ ¬ X ∈ dom ⁡ G ∖ I ↔ dom ⁡ F ∖ I ⊆ V ∖ X ↔ dom ⁡ G ∖ I ⊆ V ∖ X
9 1 8 bitri ⊢ X ∈ dom ⁡ F ∖ I ↔ X ∈ dom ⁡ G ∖ I ↔ dom ⁡ F ∖ I ⊆ V ∖ X ↔ dom ⁡ G ∖ I ⊆ V ∖ X
10 9 notbii ⊢ ¬ X ∈ dom ⁡ F ∖ I ↔ X ∈ dom ⁡ G ∖ I ↔ ¬ dom ⁡ F ∖ I ⊆ V ∖ X ↔ dom ⁡ G ∖ I ⊆ V ∖ X
11 df-xor ⊢ X ∈ dom ⁡ F ∖ I ⊻ X ∈ dom ⁡ G ∖ I ↔ ¬ X ∈ dom ⁡ F ∖ I ↔ X ∈ dom ⁡ G ∖ I
12 df-xor ⊢ dom ⁡ F ∖ I ⊆ V ∖ X ⊻ dom ⁡ G ∖ I ⊆ V ∖ X ↔ ¬ dom ⁡ F ∖ I ⊆ V ∖ X ↔ dom ⁡ G ∖ I ⊆ V ∖ X
13 10 11 12 3bitr4i ⊢ X ∈ dom ⁡ F ∖ I ⊻ X ∈ dom ⁡ G ∖ I ↔ dom ⁡ F ∖ I ⊆ V ∖ X ⊻ dom ⁡ G ∖ I ⊆ V ∖ X
14 f1omvdco2 ⊢ F : A ⟶ 1-1 onto A ∧ G : A ⟶ 1-1 onto A ∧ dom ⁡ F ∖ I ⊆ V ∖ X ⊻ dom ⁡ G ∖ I ⊆ V ∖ X → ¬ dom ⁡ F ∘ G ∖ I ⊆ V ∖ X
15 disj2 ⊢ dom ⁡ F ∘ G ∖ I ∩ X = ∅ ↔ dom ⁡ F ∘ G ∖ I ⊆ V ∖ X
16 disjsn ⊢ dom ⁡ F ∘ G ∖ I ∩ X = ∅ ↔ ¬ X ∈ dom ⁡ F ∘ G ∖ I
17 15 16 bitr3i ⊢ dom ⁡ F ∘ G ∖ I ⊆ V ∖ X ↔ ¬ X ∈ dom ⁡ F ∘ G ∖ I
18 17 con2bii ⊢ X ∈ dom ⁡ F ∘ G ∖ I ↔ ¬ dom ⁡ F ∘ G ∖ I ⊆ V ∖ X
19 14 18 sylibr ⊢ F : A ⟶ 1-1 onto A ∧ G : A ⟶ 1-1 onto A ∧ dom ⁡ F ∖ I ⊆ V ∖ X ⊻ dom ⁡ G ∖ I ⊆ V ∖ X → X ∈ dom ⁡ F ∘ G ∖ I
20 13 19 syl3an3b ⊢ F : A ⟶ 1-1 onto A ∧ G : A ⟶ 1-1 onto A ∧ X ∈ dom ⁡ F ∖ I ⊻ X ∈ dom ⁡ G ∖ I → X ∈ dom ⁡ F ∘ G ∖ I