Description: Direct proof of pwuninel avoiding functions and thus several ZF axioms. (Contributed by Stefan O'Rear, 22-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | pwuninel2 | ⊢ ( ∪ 𝐴 ∈ 𝑉 → ¬ 𝒫 ∪ 𝐴 ∈ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwnss | ⊢ ( ∪ 𝐴 ∈ 𝑉 → ¬ 𝒫 ∪ 𝐴 ⊆ ∪ 𝐴 ) | |
2 | elssuni | ⊢ ( 𝒫 ∪ 𝐴 ∈ 𝐴 → 𝒫 ∪ 𝐴 ⊆ ∪ 𝐴 ) | |
3 | 1 2 | nsyl | ⊢ ( ∪ 𝐴 ∈ 𝑉 → ¬ 𝒫 ∪ 𝐴 ∈ 𝐴 ) |