MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  compssiso Structured version   Visualization version   GIF version

Theorem compssiso 9388
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.)
Hypothesis
Ref Expression
compss.a 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴𝑥))
Assertion
Ref Expression
compssiso (𝐴𝑉𝐹 Isom [] , [] (𝒫 𝐴, 𝒫 𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑉
Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem compssiso
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 difexg 4960 . . . . 5 (𝐴𝑉 → (𝐴𝑥) ∈ V)
21ralrimivw 3105 . . . 4 (𝐴𝑉 → ∀𝑥 ∈ 𝒫 𝐴(𝐴𝑥) ∈ V)
3 compss.a . . . . 5 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴𝑥))
43fnmpt 6181 . . . 4 (∀𝑥 ∈ 𝒫 𝐴(𝐴𝑥) ∈ V → 𝐹 Fn 𝒫 𝐴)
52, 4syl 17 . . 3 (𝐴𝑉𝐹 Fn 𝒫 𝐴)
63compsscnv 9385 . . . . 5 𝐹 = 𝐹
76fneq1i 6146 . . . 4 (𝐹 Fn 𝒫 𝐴𝐹 Fn 𝒫 𝐴)
85, 7sylibr 224 . . 3 (𝐴𝑉𝐹 Fn 𝒫 𝐴)
9 dff1o4 6306 . . 3 (𝐹:𝒫 𝐴1-1-onto→𝒫 𝐴 ↔ (𝐹 Fn 𝒫 𝐴𝐹 Fn 𝒫 𝐴))
105, 8, 9sylanbrc 701 . 2 (𝐴𝑉𝐹:𝒫 𝐴1-1-onto→𝒫 𝐴)
11 elpwi 4312 . . . . . . . . 9 (𝑏 ∈ 𝒫 𝐴𝑏𝐴)
1211ad2antll 767 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → 𝑏𝐴)
133isf34lem1 9386 . . . . . . . 8 ((𝐴𝑉𝑏𝐴) → (𝐹𝑏) = (𝐴𝑏))
1412, 13syldan 488 . . . . . . 7 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐹𝑏) = (𝐴𝑏))
15 elpwi 4312 . . . . . . . . 9 (𝑎 ∈ 𝒫 𝐴𝑎𝐴)
1615ad2antrl 766 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → 𝑎𝐴)
173isf34lem1 9386 . . . . . . . 8 ((𝐴𝑉𝑎𝐴) → (𝐹𝑎) = (𝐴𝑎))
1816, 17syldan 488 . . . . . . 7 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐹𝑎) = (𝐴𝑎))
1914, 18psseq12d 3843 . . . . . 6 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ((𝐹𝑏) ⊊ (𝐹𝑎) ↔ (𝐴𝑏) ⊊ (𝐴𝑎)))
20 difss 3880 . . . . . . 7 (𝐴𝑎) ⊆ 𝐴
21 pssdifcom1 4198 . . . . . . 7 ((𝑏𝐴 ∧ (𝐴𝑎) ⊆ 𝐴) → ((𝐴𝑏) ⊊ (𝐴𝑎) ↔ (𝐴 ∖ (𝐴𝑎)) ⊊ 𝑏))
2212, 20, 21sylancl 697 . . . . . 6 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ((𝐴𝑏) ⊊ (𝐴𝑎) ↔ (𝐴 ∖ (𝐴𝑎)) ⊊ 𝑏))
23 dfss4 4001 . . . . . . . 8 (𝑎𝐴 ↔ (𝐴 ∖ (𝐴𝑎)) = 𝑎)
2416, 23sylib 208 . . . . . . 7 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝐴 ∖ (𝐴𝑎)) = 𝑎)
2524psseq1d 3841 . . . . . 6 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → ((𝐴 ∖ (𝐴𝑎)) ⊊ 𝑏𝑎𝑏))
2619, 22, 253bitrrd 295 . . . . 5 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎𝑏 ↔ (𝐹𝑏) ⊊ (𝐹𝑎)))
27 vex 3343 . . . . . 6 𝑏 ∈ V
2827brrpss 7105 . . . . 5 (𝑎 [] 𝑏𝑎𝑏)
29 fvex 6362 . . . . . 6 (𝐹𝑎) ∈ V
3029brrpss 7105 . . . . 5 ((𝐹𝑏) [] (𝐹𝑎) ↔ (𝐹𝑏) ⊊ (𝐹𝑎))
3126, 28, 303bitr4g 303 . . . 4 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎 [] 𝑏 ↔ (𝐹𝑏) [] (𝐹𝑎)))
32 relrpss 7103 . . . . 5 Rel []
3332relbrcnv 5664 . . . 4 ((𝐹𝑎) [] (𝐹𝑏) ↔ (𝐹𝑏) [] (𝐹𝑎))
3431, 33syl6bbr 278 . . 3 ((𝐴𝑉 ∧ (𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴)) → (𝑎 [] 𝑏 ↔ (𝐹𝑎) [] (𝐹𝑏)))
3534ralrimivva 3109 . 2 (𝐴𝑉 → ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎 [] 𝑏 ↔ (𝐹𝑎) [] (𝐹𝑏)))
36 df-isom 6058 . 2 (𝐹 Isom [] , [] (𝒫 𝐴, 𝒫 𝐴) ↔ (𝐹:𝒫 𝐴1-1-onto→𝒫 𝐴 ∧ ∀𝑎 ∈ 𝒫 𝐴𝑏 ∈ 𝒫 𝐴(𝑎 [] 𝑏 ↔ (𝐹𝑎) [] (𝐹𝑏))))
3710, 35, 36sylanbrc 701 1 (𝐴𝑉𝐹 Isom [] , [] (𝒫 𝐴, 𝒫 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  wcel 2139  wral 3050  Vcvv 3340  cdif 3712  wss 3715  wpss 3716  𝒫 cpw 4302   class class class wbr 4804  cmpt 4881  ccnv 5265   Fn wfn 6044  1-1-ontowf1o 6048  cfv 6049   Isom wiso 6050   [] crpss 7101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-rpss 7102
This theorem is referenced by:  isf34lem3  9389  isf34lem5  9392  isfin1-4  9401
  Copyright terms: Public domain W3C validator