This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvcnvsn

Description: Double converse of a singleton of an ordered pair. (Unlike cnvsn , this does not need any sethood assumptions on A and B .) (Contributed by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	cnvcnvsn	⊢ ^◡ ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ^◡ { ⟨ 𝐵 , 𝐴 ⟩ }

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ^◡ ^◡ { ⟨ 𝐴 , 𝐵 ⟩ }
2		relcnv	⊢ Rel ^◡ { ⟨ 𝐵 , 𝐴 ⟩ }
3		vex	⊢ 𝑥 ∈ V
4		vex	⊢ 𝑦 ∈ V
5	3 4	opelcnv	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ^◡ ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } )
6		ancom	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐴 ) )
7	3 4	opth	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
8	4 3	opth	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝐵 , 𝐴 ⟩ ↔ ( 𝑦 = 𝐵 ∧ 𝑥 = 𝐴 ) )
9	6 7 8	3bitr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝐵 , 𝐴 ⟩ )
10		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
11	10	elsn	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
12		opex	⊢ ⟨ 𝑦 , 𝑥 ⟩ ∈ V
13	12	elsn	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐵 , 𝐴 ⟩ } ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝐵 , 𝐴 ⟩ )
14	9 11 13	3bitr4i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐵 , 𝐴 ⟩ } )
15	4 3	opelcnv	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝐴 , 𝐵 ⟩ } )
16	3 4	opelcnv	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ^◡ { ⟨ 𝐵 , 𝐴 ⟩ } ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐵 , 𝐴 ⟩ } )
17	14 15 16	3bitr4i	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ^◡ { ⟨ 𝐵 , 𝐴 ⟩ } )
18	5 17	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ^◡ ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ^◡ { ⟨ 𝐵 , 𝐴 ⟩ } )
19	1 2 18	eqrelriiv	⊢ ^◡ ^◡ { ⟨ 𝐴 , 𝐵 ⟩ } = ^◡ { ⟨ 𝐵 , 𝐴 ⟩ }