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

Metamath Proof Explorer

Theorem 2pwuninel

Description: The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by NM, 27-Jun-2008)

Ref Expression
Assertion 2pwuninel ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴

Proof

Step Hyp Ref Expression
1 sdomirr ⊢ ¬ 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴
2 elssuni ⊢ ( 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ⊆ ∪ 𝐴 )
3 ssdomg ⊢ ( ∪ 𝐴 ∈ V → ( 𝒫 𝒫 ∪ 𝐴 ⊆ ∪ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ≼ ∪ 𝐴 ) )
4 canth2g ⊢ ( ∪ 𝐴 ∈ V → ∪ 𝐴 ≺ 𝒫 ∪ 𝐴 )
5 pwexb ⊢ ( ∪ 𝐴 ∈ V ↔ 𝒫 ∪ 𝐴 ∈ V )
6 canth2g ⊢ ( 𝒫 ∪ 𝐴 ∈ V → 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
7 5 6 sylbi ⊢ ( ∪ 𝐴 ∈ V → 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
8 sdomtr ⊢ ( ( ∪ 𝐴 ≺ 𝒫 ∪ 𝐴 ∧ 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) → ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
9 4 7 8 syl2anc ⊢ ( ∪ 𝐴 ∈ V → ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
10 domsdomtr ⊢ ( ( 𝒫 𝒫 ∪ 𝐴 ≼ ∪ 𝐴 ∧ ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) → 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 )
11 10 ex ⊢ ( 𝒫 𝒫 ∪ 𝐴 ≼ ∪ 𝐴 → ( ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) )
12 3 9 11 syl6ci ⊢ ( ∪ 𝐴 ∈ V → ( 𝒫 𝒫 ∪ 𝐴 ⊆ ∪ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) )
13 2 12 syl5 ⊢ ( ∪ 𝐴 ∈ V → ( 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ≺ 𝒫 𝒫 ∪ 𝐴 ) )
14 1 13 mtoi ⊢ ( ∪ 𝐴 ∈ V → ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 )
15 elex ⊢ ( 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 → 𝒫 𝒫 ∪ 𝐴 ∈ V )
16 pwexb ⊢ ( 𝒫 ∪ 𝐴 ∈ V ↔ 𝒫 𝒫 ∪ 𝐴 ∈ V )
17 5 16 bitri ⊢ ( ∪ 𝐴 ∈ V ↔ 𝒫 𝒫 ∪ 𝐴 ∈ V )
18 15 17 sylibr ⊢ ( 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 → ∪ 𝐴 ∈ V )
19 18 con3i ⊢ ( ¬ ∪ 𝐴 ∈ V → ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴 )
20 14 19 pm2.61i ⊢ ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴