Metamath Proof Explorer

Theorem kmlem15

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

Ref Expression
Hypotheses kmlem14.1 ⊢φ↔z∈y→v∈x∧y≠v∧z∈v
kmlem14.2 ⊢ψ↔z∈x→v∈z∧v∈y∧u∈z∧u∈y→u=v
kmlem14.3 ⊢χ↔∀z∈x∃!vv∈z∩y
Assertion kmlem15 ⊢¬y∈x∧χ↔∀z∃v∀u¬y∈x∧ψ

Proof

Step Hyp Ref Expression
1 kmlem14.1 ⊢φ↔z∈y→v∈x∧y≠v∧z∈v
2 kmlem14.2 ⊢ψ↔z∈x→v∈z∧v∈y∧u∈z∧u∈y→u=v
3 kmlem14.3 ⊢χ↔∀z∈x∃!vv∈z∩y
4 nfv ⊢Ⅎuv∈z∩y
5 4 eu1 ⊢∃!vv∈z∩y↔∃vv∈z∩y∧∀uuvv∈z∩y→v=u
6 elin ⊢v∈z∩y↔v∈z∧v∈y
7 clelsb1 ⊢uvv∈z∩y↔u∈z∩y
8 elin ⊢u∈z∩y↔u∈z∧u∈y
9 7 8 bitri ⊢uvv∈z∩y↔u∈z∧u∈y
10 equcom ⊢v=u↔u=v
11 9 10 imbi12i ⊢uvv∈z∩y→v=u↔u∈z∧u∈y→u=v
12 11 albii ⊢∀uuvv∈z∩y→v=u↔∀uu∈z∧u∈y→u=v
13 6 12 anbi12i ⊢v∈z∩y∧∀uuvv∈z∩y→v=u↔v∈z∧v∈y∧∀uu∈z∧u∈y→u=v
14 19.28v ⊢∀uv∈z∧v∈y∧u∈z∧u∈y→u=v↔v∈z∧v∈y∧∀uu∈z∧u∈y→u=v
15 13 14 bitr4i ⊢v∈z∩y∧∀uuvv∈z∩y→v=u↔∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
16 15 exbii ⊢∃vv∈z∩y∧∀uuvv∈z∩y→v=u↔∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
17 5 16 bitri ⊢∃!vv∈z∩y↔∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
18 17 ralbii ⊢∀z∈x∃!vv∈z∩y↔∀z∈x∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
19 df-ral ⊢∀z∈x∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v↔∀zz∈x→∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
20 2 albii ⊢∀uψ↔∀uz∈x→v∈z∧v∈y∧u∈z∧u∈y→u=v
21 19.21v ⊢∀uz∈x→v∈z∧v∈y∧u∈z∧u∈y→u=v↔z∈x→∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
22 20 21 bitri ⊢∀uψ↔z∈x→∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
23 22 exbii ⊢∃v∀uψ↔∃vz∈x→∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
24 19.37v ⊢∃vz∈x→∀uv∈z∧v∈y∧u∈z∧u∈y→u=v↔z∈x→∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
25 23 24 bitri ⊢∃v∀uψ↔z∈x→∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
26 25 albii ⊢∀z∃v∀uψ↔∀zz∈x→∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v
27 19 26 bitr4i ⊢∀z∈x∃v∀uv∈z∧v∈y∧u∈z∧u∈y→u=v↔∀z∃v∀uψ
28 3 18 27 3bitri ⊢χ↔∀z∃v∀uψ
29 28 anbi2i ⊢¬y∈x∧χ↔¬y∈x∧∀z∃v∀uψ
30 19.28v ⊢∀z¬y∈x∧∃v∀uψ↔¬y∈x∧∀z∃v∀uψ
31 19.28v ⊢∀u¬y∈x∧ψ↔¬y∈x∧∀uψ
32 31 exbii ⊢∃v∀u¬y∈x∧ψ↔∃v¬y∈x∧∀uψ
33 19.42v ⊢∃v¬y∈x∧∀uψ↔¬y∈x∧∃v∀uψ
34 32 33 bitr2i ⊢¬y∈x∧∃v∀uψ↔∃v∀u¬y∈x∧ψ
35 34 albii ⊢∀z¬y∈x∧∃v∀uψ↔∀z∃v∀u¬y∈x∧ψ
36 29 30 35 3bitr2i ⊢¬y∈x∧χ↔∀z∃v∀u¬y∈x∧ψ