Theorem compssiso

Description: Complementation is an antiautomorphism on power set lattices. (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypothesis	compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
Assertion	compssiso	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2		difexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ 𝑥 ) ∈ V )
3	2	ralrimivw	⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ V )
4	1	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝐴 ∖ 𝑥 ) ∈ V → 𝐹 Fn 𝒫 𝐴 )
5	3 4	syl	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 Fn 𝒫 𝐴 )
6	1	compsscnv	⊢ ◡ 𝐹 = 𝐹
7	6	fneq1i	⊢ ( ◡ 𝐹 Fn 𝒫 𝐴 ↔ 𝐹 Fn 𝒫 𝐴 )
8	5 7	sylibr	⊢ ( 𝐴 ∈ 𝑉 → ◡ 𝐹 Fn 𝒫 𝐴 )
9		dff1o4	⊢ ( 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 ↔ ( 𝐹 Fn 𝒫 𝐴 ∧ ◡ 𝐹 Fn 𝒫 𝐴 ) )
10	5 8 9	sylanbrc	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 )
11		elpwi	⊢ ( 𝑏 ∈ 𝒫 𝐴 → 𝑏 ⊆ 𝐴 )
12	11	ad2antll	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → 𝑏 ⊆ 𝐴 )
13	1	isf34lem1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑏 ⊆ 𝐴 ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐴 ∖ 𝑏 ) )
14	12 13	syldan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐴 ∖ 𝑏 ) )
15		elpwi	⊢ ( 𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴 )
16	15	ad2antrl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → 𝑎 ⊆ 𝐴 )
17	1	isf34lem1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑎 ⊆ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐴 ∖ 𝑎 ) )
18	16 17	syldan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐴 ∖ 𝑎 ) )
19	14 18	psseq12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( ( 𝐹 ‘ 𝑏 ) ⊊ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐴 ∖ 𝑏 ) ⊊ ( 𝐴 ∖ 𝑎 ) ) )
20		difss	⊢ ( 𝐴 ∖ 𝑎 ) ⊆ 𝐴
21		pssdifcom1	⊢ ( ( 𝑏 ⊆ 𝐴 ∧ ( 𝐴 ∖ 𝑎 ) ⊆ 𝐴 ) → ( ( 𝐴 ∖ 𝑏 ) ⊊ ( 𝐴 ∖ 𝑎 ) ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑎 ) ) ⊊ 𝑏 ) )
22	12 20 21	sylancl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( ( 𝐴 ∖ 𝑏 ) ⊊ ( 𝐴 ∖ 𝑎 ) ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑎 ) ) ⊊ 𝑏 ) )
23		dfss4	⊢ ( 𝑎 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑎 ) ) = 𝑎 )
24	16 23	sylib	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑎 ) ) = 𝑎 )
25	24	psseq1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( ( 𝐴 ∖ ( 𝐴 ∖ 𝑎 ) ) ⊊ 𝑏 ↔ 𝑎 ⊊ 𝑏 ) )
26	19 22 25	3bitrrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝑎 ⊊ 𝑏 ↔ ( 𝐹 ‘ 𝑏 ) ⊊ ( 𝐹 ‘ 𝑎 ) ) )
27		vex	⊢ 𝑏 ∈ V
28	27	brrpss	⊢ ( 𝑎 [⊊] 𝑏 ↔ 𝑎 ⊊ 𝑏 )
29		fvex	⊢ ( 𝐹 ‘ 𝑎 ) ∈ V
30	29	brrpss	⊢ ( ( 𝐹 ‘ 𝑏 ) [⊊] ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝑏 ) ⊊ ( 𝐹 ‘ 𝑎 ) )
31	26 28 30	3bitr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝑎 [⊊] 𝑏 ↔ ( 𝐹 ‘ 𝑏 ) [⊊] ( 𝐹 ‘ 𝑎 ) ) )
32		relrpss	⊢ Rel [⊊]
33	32	relbrcnv	⊢ ( ( 𝐹 ‘ 𝑎 ) ◡ [⊊] ( 𝐹 ‘ 𝑏 ) ↔ ( 𝐹 ‘ 𝑏 ) [⊊] ( 𝐹 ‘ 𝑎 ) )
34	31 33	bitr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑎 ∈ 𝒫 𝐴 ∧ 𝑏 ∈ 𝒫 𝐴 ) ) → ( 𝑎 [⊊] 𝑏 ↔ ( 𝐹 ‘ 𝑎 ) ◡ [⊊] ( 𝐹 ‘ 𝑏 ) ) )
35	34	ralrimivva	⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑎 [⊊] 𝑏 ↔ ( 𝐹 ‘ 𝑎 ) ◡ [⊊] ( 𝐹 ‘ 𝑏 ) ) )
36		df-isom	⊢ ( 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) ↔ ( 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 ∧ ∀ 𝑎 ∈ 𝒫 𝐴 ∀ 𝑏 ∈ 𝒫 𝐴 ( 𝑎 [⊊] 𝑏 ↔ ( 𝐹 ‘ 𝑎 ) ◡ [⊊] ( 𝐹 ‘ 𝑏 ) ) ) )
37	10 35 36	sylanbrc	⊢ ( 𝐴 ∈ 𝑉 → 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) )