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

Metamath Proof Explorer

Theorem compsscnv

Description: Complementation on a power set lattice is an involution. (Contributed by Mario Carneiro, 17-May-2015)

		Ref	Expression
	Hypothesis	compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
	Assertion	compsscnv	⊢ ^◡ 𝐹 = 𝐹

Proof

Step	Hyp	Ref	Expression
1		compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2		cnvopab	⊢ ^◡ { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) }
3		difeq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑦 ) )
4	3	cbvmptv	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) ) = ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) )
5		df-mpt	⊢ ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) }
6	1 4 5	3eqtri	⊢ 𝐹 = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) }
7	6	cnveqi	⊢ ^◡ 𝐹 = ^◡ { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) }
8		df-mpt	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) }
9		compsscnvlem	⊢ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) )
10		compsscnvlem	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) )
11	9 10	impbii	⊢ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) )
12	11	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) }
13	8 1 12	3eqtr4i	⊢ 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) }
14	2 7 13	3eqtr4i	⊢ ^◡ 𝐹 = 𝐹