Metamath Proof Explorer

Theorem pmtrfrn

Description: A transposition (as a kind of function) is the function transposing the two points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t ⊢ T = pmTrsp ⁡ D
pmtrrn.r ⊢ R = ran ⁡ T
pmtrfrn.p ⊢ P = dom ⁡ F ∖ I
Assertion pmtrfrn ⊢ F ∈ R → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P

Proof

Step Hyp Ref Expression
1 pmtrrn.t ⊢ T = pmTrsp ⁡ D
2 pmtrrn.r ⊢ R = ran ⁡ T
3 pmtrfrn.p ⊢ P = dom ⁡ F ∖ I
4 noel ⊢ ¬ F ∈ ∅
5 1 rnfvprc ⊢ ¬ D ∈ V → ran ⁡ T = ∅
6 2 5 syl5eq ⊢ ¬ D ∈ V → R = ∅
7 6 eleq2d ⊢ ¬ D ∈ V → F ∈ R ↔ F ∈ ∅
8 4 7 mtbiri ⊢ ¬ D ∈ V → ¬ F ∈ R
9 8 con4i ⊢ F ∈ R → D ∈ V
10 mptexg ⊢ D ∈ V → z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z ∈ V
11 10 ralrimivw ⊢ D ∈ V → ∀ w ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z ∈ V
12 eqid ⊢ w ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z = w ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z
13 12 fnmpt ⊢ ∀ w ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z ∈ V → w ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z Fn x ∈ 𝒫 D | x ≈ 2 𝑜
14 11 13 syl ⊢ D ∈ V → w ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z Fn x ∈ 𝒫 D | x ≈ 2 𝑜
15 1 pmtrfval ⊢ D ∈ V → T = w ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z
16 15 fneq1d ⊢ D ∈ V → T Fn x ∈ 𝒫 D | x ≈ 2 𝑜 ↔ w ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ w ⋃ w ∖ z z Fn x ∈ 𝒫 D | x ≈ 2 𝑜
17 14 16 mpbird ⊢ D ∈ V → T Fn x ∈ 𝒫 D | x ≈ 2 𝑜
18 fvelrnb ⊢ T Fn x ∈ 𝒫 D | x ≈ 2 𝑜 → F ∈ ran ⁡ T ↔ ∃ y ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 T ⁡ y = F
19 17 18 syl ⊢ D ∈ V → F ∈ ran ⁡ T ↔ ∃ y ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 T ⁡ y = F
20 2 eleq2i ⊢ F ∈ R ↔ F ∈ ran ⁡ T
21 breq1 ⊢ x = y → x ≈ 2 𝑜 ↔ y ≈ 2 𝑜
22 21 rexrab ⊢ ∃ y ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 T ⁡ y = F ↔ ∃ y ∈ 𝒫 D y ≈ 2 𝑜 ∧ T ⁡ y = F
23 22 bicomi ⊢ ∃ y ∈ 𝒫 D y ≈ 2 𝑜 ∧ T ⁡ y = F ↔ ∃ y ∈ x ∈ 𝒫 D | x ≈ 2 𝑜 T ⁡ y = F
24 19 20 23 3bitr4g ⊢ D ∈ V → F ∈ R ↔ ∃ y ∈ 𝒫 D y ≈ 2 𝑜 ∧ T ⁡ y = F
25 elpwi ⊢ y ∈ 𝒫 D → y ⊆ D
26 simp1 ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → D ∈ V
27 1 pmtrmvd ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → dom ⁡ T ⁡ y ∖ I = y
28 simp2 ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → y ⊆ D
29 27 28 eqsstrd ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → dom ⁡ T ⁡ y ∖ I ⊆ D
30 simp3 ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → y ≈ 2 𝑜
31 27 30 eqbrtrd ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → dom ⁡ T ⁡ y ∖ I ≈ 2 𝑜
32 26 29 31 3jca ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → D ∈ V ∧ dom ⁡ T ⁡ y ∖ I ⊆ D ∧ dom ⁡ T ⁡ y ∖ I ≈ 2 𝑜
33 27 eqcomd ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → y = dom ⁡ T ⁡ y ∖ I
34 33 fveq2d ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → T ⁡ y = T ⁡ dom ⁡ T ⁡ y ∖ I
35 32 34 jca ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → D ∈ V ∧ dom ⁡ T ⁡ y ∖ I ⊆ D ∧ dom ⁡ T ⁡ y ∖ I ≈ 2 𝑜 ∧ T ⁡ y = T ⁡ dom ⁡ T ⁡ y ∖ I
36 difeq1 ⊢ T ⁡ y = F → T ⁡ y ∖ I = F ∖ I
37 36 dmeqd ⊢ T ⁡ y = F → dom ⁡ T ⁡ y ∖ I = dom ⁡ F ∖ I
38 37 3 eqtr4di ⊢ T ⁡ y = F → dom ⁡ T ⁡ y ∖ I = P
39 sseq1 ⊢ dom ⁡ T ⁡ y ∖ I = P → dom ⁡ T ⁡ y ∖ I ⊆ D ↔ P ⊆ D
40 breq1 ⊢ dom ⁡ T ⁡ y ∖ I = P → dom ⁡ T ⁡ y ∖ I ≈ 2 𝑜 ↔ P ≈ 2 𝑜
41 39 40 3anbi23d ⊢ dom ⁡ T ⁡ y ∖ I = P → D ∈ V ∧ dom ⁡ T ⁡ y ∖ I ⊆ D ∧ dom ⁡ T ⁡ y ∖ I ≈ 2 𝑜 ↔ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜
42 41 adantl ⊢ T ⁡ y = F ∧ dom ⁡ T ⁡ y ∖ I = P → D ∈ V ∧ dom ⁡ T ⁡ y ∖ I ⊆ D ∧ dom ⁡ T ⁡ y ∖ I ≈ 2 𝑜 ↔ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜
43 simpl ⊢ T ⁡ y = F ∧ dom ⁡ T ⁡ y ∖ I = P → T ⁡ y = F
44 fveq2 ⊢ dom ⁡ T ⁡ y ∖ I = P → T ⁡ dom ⁡ T ⁡ y ∖ I = T ⁡ P
45 44 adantl ⊢ T ⁡ y = F ∧ dom ⁡ T ⁡ y ∖ I = P → T ⁡ dom ⁡ T ⁡ y ∖ I = T ⁡ P
46 43 45 eqeq12d ⊢ T ⁡ y = F ∧ dom ⁡ T ⁡ y ∖ I = P → T ⁡ y = T ⁡ dom ⁡ T ⁡ y ∖ I ↔ F = T ⁡ P
47 42 46 anbi12d ⊢ T ⁡ y = F ∧ dom ⁡ T ⁡ y ∖ I = P → D ∈ V ∧ dom ⁡ T ⁡ y ∖ I ⊆ D ∧ dom ⁡ T ⁡ y ∖ I ≈ 2 𝑜 ∧ T ⁡ y = T ⁡ dom ⁡ T ⁡ y ∖ I ↔ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
48 38 47 mpdan ⊢ T ⁡ y = F → D ∈ V ∧ dom ⁡ T ⁡ y ∖ I ⊆ D ∧ dom ⁡ T ⁡ y ∖ I ≈ 2 𝑜 ∧ T ⁡ y = T ⁡ dom ⁡ T ⁡ y ∖ I ↔ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
49 35 48 syl5ibcom ⊢ D ∈ V ∧ y ⊆ D ∧ y ≈ 2 𝑜 → T ⁡ y = F → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
50 49 3exp ⊢ D ∈ V → y ⊆ D → y ≈ 2 𝑜 → T ⁡ y = F → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
51 50 imp4a ⊢ D ∈ V → y ⊆ D → y ≈ 2 𝑜 ∧ T ⁡ y = F → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
52 25 51 syl5 ⊢ D ∈ V → y ∈ 𝒫 D → y ≈ 2 𝑜 ∧ T ⁡ y = F → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
53 52 rexlimdv ⊢ D ∈ V → ∃ y ∈ 𝒫 D y ≈ 2 𝑜 ∧ T ⁡ y = F → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
54 24 53 sylbid ⊢ D ∈ V → F ∈ R → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
55 9 54 mpcom ⊢ F ∈ R → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P