Step |
Hyp |
Ref |
Expression |
1 |
|
kmlem14.1 |
⊢ ( 𝜑 ↔ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) ) |
2 |
|
kmlem14.2 |
⊢ ( 𝜓 ↔ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) ) |
3 |
|
kmlem14.3 |
⊢ ( 𝜒 ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) |
4 |
1 2 3
|
kmlem14 |
⊢ ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ) |
5 |
1 2 3
|
kmlem15 |
⊢ ( ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) |
6 |
5
|
exbii |
⊢ ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) |
7 |
4 6
|
orbi12i |
⊢ ( ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ( ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
8 |
|
19.43 |
⊢ ( ∃ 𝑦 ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
9 |
|
pm3.24 |
⊢ ¬ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) |
10 |
|
simpl |
⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) |
11 |
10
|
sps |
⊢ ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) |
12 |
11
|
exlimivv |
⊢ ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) |
13 |
|
simpl |
⊢ ( ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) → ¬ 𝑦 ∈ 𝑥 ) |
14 |
13
|
sps |
⊢ ( ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) → ¬ 𝑦 ∈ 𝑥 ) |
15 |
14
|
exlimivv |
⊢ ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) → ¬ 𝑦 ∈ 𝑥 ) |
16 |
12 15
|
anim12i |
⊢ ( ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) → ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) ) |
17 |
9 16
|
mto |
⊢ ¬ ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) |
18 |
|
19.33b |
⊢ ( ¬ ( ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) → ( ∀ 𝑧 ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) ) |
19 |
17 18
|
ax-mp |
⊢ ( ∀ 𝑧 ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
20 |
10
|
exlimiv |
⊢ ( ∃ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑥 ) |
21 |
13
|
exlimiv |
⊢ ( ∃ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) → ¬ 𝑦 ∈ 𝑥 ) |
22 |
20 21
|
anim12i |
⊢ ( ( ∃ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) → ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ 𝑥 ) ) |
23 |
9 22
|
mto |
⊢ ¬ ( ∃ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) |
24 |
|
19.33b |
⊢ ( ¬ ( ∃ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∧ ∃ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) → ( ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) ) |
25 |
23 24
|
ax-mp |
⊢ ( ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
26 |
25
|
exbii |
⊢ ( ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∃ 𝑣 ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
27 |
|
19.43 |
⊢ ( ∃ 𝑣 ( ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
28 |
26 27
|
bitr2i |
⊢ ( ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
29 |
28
|
albii |
⊢ ( ∀ 𝑧 ( ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
30 |
19 29
|
bitr3i |
⊢ ( ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
31 |
30
|
exbii |
⊢ ( ∃ 𝑦 ( ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |
32 |
7 8 31
|
3bitr2i |
⊢ ( ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) ) |