negiso

Description: Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Hypothesis	negiso.1	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ - 𝑥 )
	Assertion	negiso	⊢ ( 𝐹 Isom < , ^◡ < ( ℝ , ℝ ) ∧ ^◡ 𝐹 = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		negiso.1	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ - 𝑥 )
2		simpr	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
3	2	renegcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → - 𝑥 ∈ ℝ )
4		simpr	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
5	4	renegcld	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → - 𝑦 ∈ ℝ )
6		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
7		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
8		negcon2	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
9	6 7 8	syl2an	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
10	9	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
11	1 3 5 10	f1ocnv2d	⊢ ( ⊤ → ( 𝐹 : ℝ –1-1-onto→ ℝ ∧ ^◡ 𝐹 = ( 𝑦 ∈ ℝ ↦ - 𝑦 ) ) )
12	11	mptru	⊢ ( 𝐹 : ℝ –1-1-onto→ ℝ ∧ ^◡ 𝐹 = ( 𝑦 ∈ ℝ ↦ - 𝑦 ) )
13	12	simpli	⊢ 𝐹 : ℝ –1-1-onto→ ℝ
14		ltneg	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 < 𝑦 ↔ - 𝑦 < - 𝑧 ) )
15		negex	⊢ - 𝑧 ∈ V
16		negex	⊢ - 𝑦 ∈ V
17	15 16	brcnv	⊢ ( - 𝑧 ^◡ < - 𝑦 ↔ - 𝑦 < - 𝑧 )
18	14 17	bitr4di	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 < 𝑦 ↔ - 𝑧 ^◡ < - 𝑦 ) )
19		negeq	⊢ ( 𝑥 = 𝑧 → - 𝑥 = - 𝑧 )
20	19 1 15	fvmpt	⊢ ( 𝑧 ∈ ℝ → ( 𝐹 ‘ 𝑧 ) = - 𝑧 )
21		negeq	⊢ ( 𝑥 = 𝑦 → - 𝑥 = - 𝑦 )
22	21 1 16	fvmpt	⊢ ( 𝑦 ∈ ℝ → ( 𝐹 ‘ 𝑦 ) = - 𝑦 )
23	20 22	breqan12d	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑧 ) ^◡ < ( 𝐹 ‘ 𝑦 ) ↔ - 𝑧 ^◡ < - 𝑦 ) )
24	18 23	bitr4d	⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 < 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) ^◡ < ( 𝐹 ‘ 𝑦 ) ) )
25	24	rgen2	⊢ ∀ 𝑧 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑧 < 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) ^◡ < ( 𝐹 ‘ 𝑦 ) )
26		df-isom	⊢ ( 𝐹 Isom < , ^◡ < ( ℝ , ℝ ) ↔ ( 𝐹 : ℝ –1-1-onto→ ℝ ∧ ∀ 𝑧 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑧 < 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) ^◡ < ( 𝐹 ‘ 𝑦 ) ) ) )
27	13 25 26	mpbir2an	⊢ 𝐹 Isom < , ^◡ < ( ℝ , ℝ )
28		negeq	⊢ ( 𝑦 = 𝑥 → - 𝑦 = - 𝑥 )
29	28	cbvmptv	⊢ ( 𝑦 ∈ ℝ ↦ - 𝑦 ) = ( 𝑥 ∈ ℝ ↦ - 𝑥 )
30	12	simpri	⊢ ^◡ 𝐹 = ( 𝑦 ∈ ℝ ↦ - 𝑦 )
31	29 30 1	3eqtr4i	⊢ ^◡ 𝐹 = 𝐹
32	27 31	pm3.2i	⊢ ( 𝐹 Isom < , ^◡ < ( ℝ , ℝ ) ∧ ^◡ 𝐹 = 𝐹 )

Metamath Proof Explorer

Theorem negiso

Proof