kmlem13

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

		Ref	Expression
	Hypothesis	kmlem9.1	⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
	Assertion	kmlem13	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		kmlem9.1	⊢ 𝐴 = { 𝑢 ∣ ∃ 𝑡 ∈ 𝑥 𝑢 = ( 𝑡 ∖ ∪ ( 𝑥 ∖ { 𝑡 } ) ) }
2		kmlem1	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ 𝑥 ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
3		raleq	⊢ ( 𝑥 = ℎ → ( ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
4	3	raleqbi1dv	⊢ ( 𝑥 = ℎ → ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) )
5		raleq	⊢ ( 𝑥 = ℎ → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
6	5	exbidv	⊢ ( 𝑥 = ℎ → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
7	4 6	imbi12d	⊢ ( 𝑥 = ℎ → ( ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ) )
8	7	cbvalvw	⊢ ( ∀ 𝑥 ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) ↔ ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
9	1	kmlem10	⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
10		ineq2	⊢ ( 𝑦 = 𝑔 → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ 𝑔 ) )
11	10	eleq2d	⊢ ( 𝑦 = 𝑔 → ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) )
12	11	eubidv	⊢ ( 𝑦 = 𝑔 → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) )
13	12	imbi2d	⊢ ( 𝑦 = 𝑔 → ( ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) ) )
14	13	ralbidv	⊢ ( 𝑦 = 𝑔 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) ) )
15	14	cbvexvw	⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∃ 𝑔 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) )
16		kmlem3	⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
17		ralinexa	⊢ ( ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ¬ ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
18	17	rexbii	⊢ ( ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∃ 𝑣 ∈ 𝑧 ¬ ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
19		rexnal	⊢ ( ∃ 𝑣 ∈ 𝑧 ¬ ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ¬ ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
20	16 18 19	3bitri	⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ¬ ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
21	20	ralbii	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ∀ 𝑧 ∈ 𝑥 ¬ ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
22		ralnex	⊢ ( ∀ 𝑧 ∈ 𝑥 ¬ ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
23	21 22	bitri	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
24	1	kmlem12	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) ) )
25		vex	⊢ 𝑔 ∈ V
26	25	inex1	⊢ ( 𝑔 ∩ ∪ 𝐴 ) ∈ V
27		ineq2	⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( 𝑧 ∩ 𝑦 ) = ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) )
28	27	eleq2d	⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) )
29	28	eubidv	⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) )
30	29	imbi2d	⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) ) )
31	30	ralbidv	⊢ ( 𝑦 = ( 𝑔 ∩ ∪ 𝐴 ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) ) )
32	26 31	spcev	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ ( 𝑔 ∩ ∪ 𝐴 ) ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
33	24 32	syl6	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
34	33	exlimdv	⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ( ∃ 𝑔 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
35	34	com12	⊢ ( ∃ 𝑔 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
36	23 35	biimtrrid	⊢ ( ∃ 𝑔 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑔 ) ) → ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
37	15 36	sylbi	⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
38	9 37	syl	⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
39	38	alrimiv	⊢ ( ∀ ℎ ( ∀ 𝑧 ∈ ℎ ∀ 𝑤 ∈ ℎ ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ ℎ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
40	8 39	sylbi	⊢ ( ∀ 𝑥 ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
41	2 40	syl	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) → ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
42		kmlem7	⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
43	42	imim1i	⊢ ( ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
44		biimt	⊢ ( 𝑧 ≠ ∅ → ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
45	44	ralimi	⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ → ∀ 𝑧 ∈ 𝑥 ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
46		ralbi	⊢ ( ∀ 𝑧 ∈ 𝑥 ( ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
47	45 46	syl	⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ → ( ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
48	47	exbidv	⊢ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
49	48	adantr	⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
50	49	pm5.74i	⊢ ( ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )
51	43 50	sylibr	⊢ ( ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
52	51	alimi	⊢ ( ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) → ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) )
53	41 52	impbii	⊢ ( ∀ 𝑥 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ( 𝑧 ∩ 𝑤 ) = ∅ ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ↔ ∀ 𝑥 ( ¬ ∃ 𝑧 ∈ 𝑥 ∀ 𝑣 ∈ 𝑧 ∃ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑣 𝑣 ∈ ( 𝑧 ∩ 𝑦 ) ) ) )

Metamath Proof Explorer

Theorem kmlem13

Proof