Step |
Hyp |
Ref |
Expression |
1 |
|
df-rex |
⊢ ( ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ Univ ∧ 𝑥 ∈ 𝑦 ) ) |
2 |
|
ancom |
⊢ ( ( 𝑦 ∈ Univ ∧ 𝑥 ∈ 𝑦 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ Univ ) ) |
3 |
|
biid |
⊢ ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) |
4 |
|
grumnueq |
⊢ Univ = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) } |
5 |
4
|
ismnu |
⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ Univ ↔ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑦 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) ) |
6 |
5
|
elv |
⊢ ( 𝑦 ∈ Univ ↔ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑦 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
7 |
|
ismnuprim |
⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝑧 ( ∃ 𝑣 ∈ 𝑦 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) ) |
8 |
6 7
|
bitri |
⊢ ( 𝑦 ∈ Univ ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) ) |
9 |
3 8
|
expandan |
⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ Univ ) ↔ ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) ) ) |
10 |
2 9
|
bitri |
⊢ ( ( 𝑦 ∈ Univ ∧ 𝑥 ∈ 𝑦 ) ↔ ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) ) ) |
11 |
10
|
expandexn |
⊢ ( ∃ 𝑦 ( 𝑦 ∈ Univ ∧ 𝑥 ∈ 𝑦 ) ↔ ¬ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) ) ) |
12 |
1 11
|
bitri |
⊢ ( ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ¬ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) ) ) |
13 |
12
|
albii |
⊢ ( ∀ 𝑥 ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ¬ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑓 ¬ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ∀ 𝑣 ¬ ( ( ∀ 𝑡 ( 𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑧 ) → ¬ ( 𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑤 ) ) → ¬ ∀ 𝑖 ( 𝑖 ∈ 𝑧 → ( 𝑣 ∈ 𝑦 → ( 𝑖 ∈ 𝑣 → ( 𝑣 ∈ 𝑓 → ¬ ∀ 𝑢 ( 𝑢 ∈ 𝑓 → ( 𝑖 ∈ 𝑢 → ¬ ∀ 𝑜 ( 𝑜 ∈ 𝑢 → ∀ 𝑠 ( 𝑠 ∈ 𝑜 → 𝑠 ∈ 𝑤 ) ) ) ) ) ) ) ) ) ) ) ) ) |