Metamath Proof Explorer

Theorem kmlem8

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 4-Apr-2004)

Ref Expression
Assertion kmlem8 ⊢¬∃z∈u∀w∈zψ→∃y∀z∈uz≠∅→∃!ww∈z∩y↔∃z∈u∀w∈zψ∨∃y¬y∈u∧∀z∈u∃!ww∈z∩y

Proof

Step Hyp Ref Expression
1 ralnex ⊢∀z∈u¬∀w∈zψ↔¬∃z∈u∀w∈zψ
2 df-rex ⊢∃w∈z¬ψ↔∃ww∈z∧¬ψ
3 rexnal ⊢∃w∈z¬ψ↔¬∀w∈zψ
4 2 3 bitr3i ⊢∃ww∈z∧¬ψ↔¬∀w∈zψ
5 exsimpl ⊢∃ww∈z∧¬ψ→∃ww∈z
6 n0 ⊢z≠∅↔∃ww∈z
7 5 6 sylibr ⊢∃ww∈z∧¬ψ→z≠∅
8 4 7 sylbir ⊢¬∀w∈zψ→z≠∅
9 8 ralimi ⊢∀z∈u¬∀w∈zψ→∀z∈uz≠∅
10 1 9 sylbir ⊢¬∃z∈u∀w∈zψ→∀z∈uz≠∅
11 kmlem2 ⊢∃y∀z∈uz≠∅→∃!ww∈z∩y↔∃y¬y∈u∧∀z∈uz≠∅→∃!ww∈z∩y
12 biimt ⊢z≠∅→∃!ww∈z∩y↔z≠∅→∃!ww∈z∩y
13 12 ralimi ⊢∀z∈uz≠∅→∀z∈u∃!ww∈z∩y↔z≠∅→∃!ww∈z∩y
14 ralbi ⊢∀z∈u∃!ww∈z∩y↔z≠∅→∃!ww∈z∩y→∀z∈u∃!ww∈z∩y↔∀z∈uz≠∅→∃!ww∈z∩y
15 13 14 syl ⊢∀z∈uz≠∅→∀z∈u∃!ww∈z∩y↔∀z∈uz≠∅→∃!ww∈z∩y
16 15 anbi2d ⊢∀z∈uz≠∅→¬y∈u∧∀z∈u∃!ww∈z∩y↔¬y∈u∧∀z∈uz≠∅→∃!ww∈z∩y
17 16 exbidv ⊢∀z∈uz≠∅→∃y¬y∈u∧∀z∈u∃!ww∈z∩y↔∃y¬y∈u∧∀z∈uz≠∅→∃!ww∈z∩y
18 11 17 bitr4id ⊢∀z∈uz≠∅→∃y∀z∈uz≠∅→∃!ww∈z∩y↔∃y¬y∈u∧∀z∈u∃!ww∈z∩y
19 10 18 syl ⊢¬∃z∈u∀w∈zψ→∃y∀z∈uz≠∅→∃!ww∈z∩y↔∃y¬y∈u∧∀z∈u∃!ww∈z∩y
20 19 pm5.74i ⊢¬∃z∈u∀w∈zψ→∃y∀z∈uz≠∅→∃!ww∈z∩y↔¬∃z∈u∀w∈zψ→∃y¬y∈u∧∀z∈u∃!ww∈z∩y
21 pm4.64 ⊢¬∃z∈u∀w∈zψ→∃y¬y∈u∧∀z∈u∃!ww∈z∩y↔∃z∈u∀w∈zψ∨∃y¬y∈u∧∀z∈u∃!ww∈z∩y
22 20 21 bitri ⊢¬∃z∈u∀w∈zψ→∃y∀z∈uz≠∅→∃!ww∈z∩y↔∃z∈u∀w∈zψ∨∃y¬y∈u∧∀z∈u∃!ww∈z∩y