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

Metamath Proof Explorer

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 [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) )