Theorem kmlem16 3595

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4 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
kmlem16	⊢ ((∃z ∈ x ∀v ∈ z ∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ∨ ∃y(¬ y ∈ x ∧ χ)) ↔ ∃y∀z∃v∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)))

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

Proof of Theorem kmlem16

Step	Hyp	Ref	Expression
1		kmlem14.1	. . . 4 ⊢ (φ ↔ (z ∈ y → ((v ∈ x ∧ ¬ y = v) ∧ z ∈ v)))
2		kmlem14.2	. . . 4 ⊢ (ψ ↔ (z ∈ x → ((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
3		kmlem14.3	. . . 4 ⊢ (χ ↔ ∀z ∈ x ∃!v v ∈ (z ∩ y))
4	1, 2, 3	kmlem14 3593	. . 3 ⊢ (∃z ∈ x ∀v ∈ z ∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ↔ ∃y∀z∃v∀u(y ∈ x ∧ φ))
5	1, 2, 3	kmlem15 3594	. . . 4 ⊢ ((¬ y ∈ x ∧ χ) ↔ ∀z∃v∀u(¬ y ∈ x ∧ ψ))
6	5	biex 733	. . 3 ⊢ (∃y(¬ y ∈ x ∧ χ) ↔ ∃y∀z∃v∀u(¬ y ∈ x ∧ ψ))
7	4, 6	orbi12i 216	. 2 ⊢ ((∃z ∈ x ∀v ∈ z ∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ∨ ∃y(¬ y ∈ x ∧ χ)) ↔ (∃y∀z∃v∀u(y ∈ x ∧ φ) ∨ ∃y∀z∃v∀u(¬ y ∈ x ∧ ψ)))
8		19.43 767	. . 3 ⊢ (∃y(∀z∃v∀u(y ∈ x ∧ φ) ∨ ∀z∃v∀u(¬ y ∈ x ∧ ψ)) ↔ (∃y∀z∃v∀u(y ∈ x ∧ φ) ∨ ∃y∀z∃v∀u(¬ y ∈ x ∧ ψ)))
9		pm3.24 496	. . . . . . 7 ⊢ ¬ (y ∈ x ∧ ¬ y ∈ x)
10		pm3.26 256	. . . . . . . . . 10 ⊢ ((y ∈ x ∧ φ) → y ∈ x)
11	10	a4s 682	. . . . . . . . 9 ⊢ (∀u(y ∈ x ∧ φ) → y ∈ x)
12	11	19.23aivv 953	. . . . . . . 8 ⊢ (∃z∃v∀u(y ∈ x ∧ φ) → y ∈ x)
13		pm3.26 256	. . . . . . . . . 10 ⊢ ((¬ y ∈ x ∧ ψ) → ¬ y ∈ x)
14	13	a4s 682	. . . . . . . . 9 ⊢ (∀u(¬ y ∈ x ∧ ψ) → ¬ y ∈ x)
15	14	19.23aivv 953	. . . . . . . 8 ⊢ (∃z∃v∀u(¬ y ∈ x ∧ ψ) → ¬ y ∈ x)
16	12, 15	anim12i 268	. . . . . . 7 ⊢ ((∃z∃v∀u(y ∈ x ∧ φ) ∧ ∃z∃v∀u(¬ y ∈ x ∧ ψ)) → (y ∈ x ∧ ¬ y ∈ x))
17	9, 16	mto 93	. . . . . 6 ⊢ ¬ (∃z∃v∀u(y ∈ x ∧ φ) ∧ ∃z∃v∀u(¬ y ∈ x ∧ ψ))
18		19.33b 771	. . . . . 6 ⊢ (¬ (∃z∃v∀u(y ∈ x ∧ φ) ∧ ∃z∃v∀u(¬ y ∈ x ∧ ψ)) → (∀z(∃v∀u(y ∈ x ∧ φ) ∨ ∃v∀u(¬ y ∈ x ∧ ψ)) ↔ (∀z∃v∀u(y ∈ x ∧ φ) ∨ ∀z∃v∀u(¬ y ∈ x ∧ ψ))))
19	17, 18	ax-mp 6	. . . . 5 ⊢ (∀z(∃v∀u(y ∈ x ∧ φ) ∨ ∃v∀u(¬ y ∈ x ∧ ψ)) ↔ (∀z∃v∀u(y ∈ x ∧ φ) ∨ ∀z∃v∀u(¬ y ∈ x ∧ ψ)))
20	10	19.23aiv 952	. . . . . . . . . . 11 ⊢ (∃u(y ∈ x ∧ φ) → y ∈ x)
21	13	19.23aiv 952	. . . . . . . . . . 11 ⊢ (∃u(¬ y ∈ x ∧ ψ) → ¬ y ∈ x)
22	20, 21	anim12i 268	. . . . . . . . . 10 ⊢ ((∃u(y ∈ x ∧ φ) ∧ ∃u(¬ y ∈ x ∧ ψ)) → (y ∈ x ∧ ¬ y ∈ x))
23	9, 22	mto 93	. . . . . . . . 9 ⊢ ¬ (∃u(y ∈ x ∧ φ) ∧ ∃u(¬ y ∈ x ∧ ψ))
24		19.33b 771	. . . . . . . . 9 ⊢ (¬ (∃u(y ∈ x ∧ φ) ∧ ∃u(¬ y ∈ x ∧ ψ)) → (∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)) ↔ (∀u(y ∈ x ∧ φ) ∨ ∀u(¬ y ∈ x ∧ ψ))))
25	23, 24	ax-mp 6	. . . . . . . 8 ⊢ (∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)) ↔ (∀u(y ∈ x ∧ φ) ∨ ∀u(¬ y ∈ x ∧ ψ)))
26	25	biex 733	. . . . . . 7 ⊢ (∃v∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)) ↔ ∃v(∀u(y ∈ x ∧ φ) ∨ ∀u(¬ y ∈ x ∧ ψ)))
27		19.43 767	. . . . . . 7 ⊢ (∃v(∀u(y ∈ x ∧ φ) ∨ ∀u(¬ y ∈ x ∧ ψ)) ↔ (∃v∀u(y ∈ x ∧ φ) ∨ ∃v∀u(¬ y ∈ x ∧ ψ)))
28	26, 27	bitr2 152	. . . . . 6 ⊢ ((∃v∀u(y ∈ x ∧ φ) ∨ ∃v∀u(¬ y ∈ x ∧ ψ)) ↔ ∃v∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)))
29	28	bial 695	. . . . 5 ⊢ (∀z(∃v∀u(y ∈ x ∧ φ) ∨ ∃v∀u(¬ y ∈ x ∧ ψ)) ↔ ∀z∃v∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)))
30	19, 29	bitr3 153	. . . 4 ⊢ ((∀z∃v∀u(y ∈ x ∧ φ) ∨ ∀z∃v∀u(¬ y ∈ x ∧ ψ)) ↔ ∀z∃v∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)))
31	30	biex 733	. . 3 ⊢ (∃y(∀z∃v∀u(y ∈ x ∧ φ) ∨ ∀z∃v∀u(¬ y ∈ x ∧ ψ)) ↔ ∃y∀z∃v∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)))
32	8, 31	bitr3 153	. 2 ⊢ ((∃y∀z∃v∀u(y ∈ x ∧ φ) ∨ ∃y∀z∃v∀u(¬ y ∈ x ∧ ψ)) ↔ ∃y∀z∃v∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)))
33	7, 32	bitr 151	1 ⊢ ((∃z ∈ x ∀v ∈ z ∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ∨ ∃y(¬ y ∈ x ∧ χ)) ↔ ∃y∀z∃v∀u((y ∈ x ∧ φ) ∨ (¬ y ∈ x ∧ ψ)))

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

This theorem is referenced by:  aceqkm 3596

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-rex 1206  df-v 1349  df-in 1491

metamath.org