Theorem kmlem16

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

	Ref	Expression
Hypotheses	kmlem14.1	⊢ ( 𝜑 ↔ ( 𝑧 ∈ 𝑦 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑣 ) ) )
	kmlem14.2	⊢ ( 𝜓 ↔ ( 𝑧 ∈ 𝑥 → ( ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦 ) ∧ ( ( 𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦 ) → 𝑢 = 𝑣 ) ) ) )
	kmlem14.3	⊢ ( 𝜒 ↔ ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) )
Assertion	kmlem16	⊢ ( ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )

Proof

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	⊢ ( ( ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ∨ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜒 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∃ 𝑣 ∀ 𝑢 ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ∨ ( ¬ 𝑦 ∈ 𝑥 ∧ 𝜓 ) ) )