Metamath Proof Explorer

Theorem pmtrf

Description: Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015)

		Ref	Expression
	Hypothesis	pmtrfval.t	$⊢ T = pmTrsp (D)$
	Assertion	pmtrf	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to T (P) : D ⟶ D$

Proof

Step	Hyp	Ref	Expression
1		pmtrfval.t	$⊢ T = pmTrsp (D)$
2	1	pmtrval	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to T (P) = (z \in D ⟼ if (z \in P, ⋃ (P ∖ \{z\}), z))$
3		simpll2	$⊢ (((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \land z \in P) \to P \subseteq D$
4		1onn	$⊢ 1_{𝑜} \in ω$
5		simpll3	$⊢ (((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \land z \in P) \to P \approx 2_{𝑜}$
6		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
7	5 6	breqtrdi	$⊢ (((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \land z \in P) \to P \approx suc 1_{𝑜}$
8		simpr	$⊢ (((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \land z \in P) \to z \in P$
9		dif1ennn	$⊢ (1_{𝑜} \in ω \land P \approx suc 1_{𝑜} \land z \in P) \to (P ∖ \{z\}) \approx 1_{𝑜}$
10	4 7 8 9	mp3an2i	$⊢ (((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \land z \in P) \to (P ∖ \{z\}) \approx 1_{𝑜}$
11		en1uniel	$⊢ (P ∖ \{z\}) \approx 1_{𝑜} \to ⋃ (P ∖ \{z\}) \in (P ∖ \{z\})$
12		eldifi	$⊢ ⋃ (P ∖ \{z\}) \in (P ∖ \{z\}) \to ⋃ (P ∖ \{z\}) \in P$
13	10 11 12	3syl	$⊢ (((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \land z \in P) \to ⋃ (P ∖ \{z\}) \in P$
14	3 13	sseldd	$⊢ (((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \land z \in P) \to ⋃ (P ∖ \{z\}) \in D$
15		simplr	$⊢ (((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \land \neg z \in P) \to z \in D$
16	14 15	ifclda	$⊢ ((D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \land z \in D) \to if (z \in P, ⋃ (P ∖ \{z\}), z) \in D$
17	2 16	fmpt3d	$⊢ (D \in V \land P \subseteq D \land P \approx 2_{𝑜}) \to T (P) : D ⟶ D$