Theorem kmlem15 3594

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4.

Hypotheses

Ref	Expression
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 ∃!v v ∈ (z ∩ y))

Assertion

Ref	Expression
kmlem15	⊢ ((¬ y ∈ x ∧ χ) ↔ ∀z∃v∀u(¬ y ∈ x ∧ ψ))

Distinct variable group(s):   x,y,z,v,u   φ,u

Proof of Theorem kmlem15

Step	Hyp	Ref	Expression
1		kmlem14.3	. . . 4 ⊢ (χ ↔ ∀z ∈ x ∃!v v ∈ (z ∩ y))
2		ax-17 925	. . . . . . 7 ⊢ (v ∈ (z ∩ y) → ∀u v ∈ (z ∩ y))
3	2	eu1 1019	. . . . . 6 ⊢ (∃!v v ∈ (z ∩ y) ↔ ∃v(v ∈ (z ∩ y) ∧ ∀u([u / v]v ∈ (z ∩ y) → v = u)))
4		elin 1635	. . . . . . . . 9 ⊢ (v ∈ (z ∩ y) ↔ (v ∈ z ∧ v ∈ y))
5		ax-17 925	. . . . . . . . . . . . 13 ⊢ (u ∈ (z ∩ y) → ∀v u ∈ (z ∩ y))
6		eleq1 1149	. . . . . . . . . . . . 13 ⊢ (v = u → (v ∈ (z ∩ y) ↔ u ∈ (z ∩ y)))
7	5, 6	sbie 904	. . . . . . . . . . . 12 ⊢ ([u / v]v ∈ (z ∩ y) ↔ u ∈ (z ∩ y))
8		elin 1635	. . . . . . . . . . . 12 ⊢ (u ∈ (z ∩ y) ↔ (u ∈ z ∧ u ∈ y))
9	7, 8	bitr 151	. . . . . . . . . . 11 ⊢ ([u / v]v ∈ (z ∩ y) ↔ (u ∈ z ∧ u ∈ y))
10		cleqcom 1103	. . . . . . . . . . 11 ⊢ (v = u ↔ u = v)
11	9, 10	imbi12i 163	. . . . . . . . . 10 ⊢ (([u / v]v ∈ (z ∩ y) → v = u) ↔ ((u ∈ z ∧ u ∈ y) → u = v))
12	11	bial 695	. . . . . . . . 9 ⊢ (∀u([u / v]v ∈ (z ∩ y) → v = u) ↔ ∀u((u ∈ z ∧ u ∈ y) → u = v))
13	4, 12	anbi12i 369	. . . . . . . 8 ⊢ ((v ∈ (z ∩ y) ∧ ∀u([u / v]v ∈ (z ∩ y) → v = u)) ↔ ((v ∈ z ∧ v ∈ y) ∧ ∀u((u ∈ z ∧ u ∈ y) → u = v)))
14		19.28v 957	. . . . . . . 8 ⊢ (∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v)) ↔ ((v ∈ z ∧ v ∈ y) ∧ ∀u((u ∈ z ∧ u ∈ y) → u = v)))
15	13, 14	bitr4 154	. . . . . . 7 ⊢ ((v ∈ (z ∩ y) ∧ ∀u([u / v]v ∈ (z ∩ y) → v = u)) ↔ ∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v)))
16	15	biex 733	. . . . . 6 ⊢ (∃v(v ∈ (z ∩ y) ∧ ∀u([u / v]v ∈ (z ∩ y) → v = u)) ↔ ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v)))
17	3, 16	bitr 151	. . . . 5 ⊢ (∃!v v ∈ (z ∩ y) ↔ ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v)))
18	17	biral 1223	. . . 4 ⊢ (∀z ∈ x ∃!v v ∈ (z ∩ y) ↔ ∀z ∈ x ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v)))
19		df-ral 1205	. . . . 5 ⊢ (∀z ∈ x ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v)) ↔ ∀z(z ∈ x → ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
20		kmlem14.2	. . . . . . . . . 10 ⊢ (ψ ↔ (z ∈ x → ((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
21	20	bial 695	. . . . . . . . 9 ⊢ (∀uψ ↔ ∀u(z ∈ x → ((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
22		19.21v 942	. . . . . . . . 9 ⊢ (∀u(z ∈ x → ((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))) ↔ (z ∈ x → ∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
23	21, 22	bitr 151	. . . . . . . 8 ⊢ (∀uψ ↔ (z ∈ x → ∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
24	23	biex 733	. . . . . . 7 ⊢ (∃v∀uψ ↔ ∃v(z ∈ x → ∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
25		19.37v 961	. . . . . . 7 ⊢ (∃v(z ∈ x → ∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))) ↔ (z ∈ x → ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
26	24, 25	bitr 151	. . . . . 6 ⊢ (∃v∀uψ ↔ (z ∈ x → ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
27	26	bial 695	. . . . 5 ⊢ (∀z∃v∀uψ ↔ ∀z(z ∈ x → ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
28	19, 27	bitr4 154	. . . 4 ⊢ (∀z ∈ x ∃v∀u((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v)) ↔ ∀z∃v∀uψ)
29	1, 18, 28	3bitr 155	. . 3 ⊢ (χ ↔ ∀z∃v∀uψ)
30	29	anbi2i 367	. 2 ⊢ ((¬ y ∈ x ∧ χ) ↔ (¬ y ∈ x ∧ ∀z∃v∀uψ))
31		19.28v 957	. . 3 ⊢ (∀z(¬ y ∈ x ∧ ∃v∀uψ) ↔ (¬ y ∈ x ∧ ∀z∃v∀uψ))
32		19.28v 957	. . . . . 6 ⊢ (∀u(¬ y ∈ x ∧ ψ) ↔ (¬ y ∈ x ∧ ∀uψ))
33	32	biex 733	. . . . 5 ⊢ (∃v∀u(¬ y ∈ x ∧ ψ) ↔ ∃v(¬ y ∈ x ∧ ∀uψ))
34		19.42v 966	. . . . 5 ⊢ (∃v(¬ y ∈ x ∧ ∀uψ) ↔ (¬ y ∈ x ∧ ∃v∀uψ))
35	33, 34	bitr2 152	. . . 4 ⊢ ((¬ y ∈ x ∧ ∃v∀uψ) ↔ ∃v∀u(¬ y ∈ x ∧ ψ))
36	35	bial 695	. . 3 ⊢ (∀z(¬ y ∈ x ∧ ∃v∀uψ) ↔ ∀z∃v∀u(¬ y ∈ x ∧ ψ))
37	31, 36	bitr3 153	. 2 ⊢ ((¬ y ∈ x ∧ ∀z∃v∀uψ) ↔ ∀z∃v∀u(¬ y ∈ x ∧ ψ))
38	30, 37	bitr 151	1 ⊢ ((¬ y ∈ x ∧ χ) ↔ ∀z∃v∀u(¬ y ∈ x ∧ ψ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803  [wsb 852  ∃!weu 1007   ∈ wcel 1092  ∀wral 1201   ∩ cin 1486

This theorem is referenced by:  kmlem16 3595

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-v 1349  df-in 1491

metamath.org