Theorem bnj1174

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1174.3	⊢ 𝐶 = ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 )
	bnj1174.59	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) )
	bnj1174.74	⊢ ( 𝜃 → ( 𝑤 𝑅 𝑧 → 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
Assertion	bnj1174	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1174.3	⊢ 𝐶 = ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 )
2		bnj1174.59	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) )
3		bnj1174.74	⊢ ( 𝜃 → ( 𝑤 𝑅 𝑧 → 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
4	1	eleq2i	⊢ ( 𝑤 ∈ 𝐶 ↔ 𝑤 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) )
5	4	notbii	⊢ ( ¬ 𝑤 ∈ 𝐶 ↔ ¬ 𝑤 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) )
6		ianor	⊢ ( ¬ ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑤 ∈ 𝐵 ) ↔ ( ¬ 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∨ ¬ 𝑤 ∈ 𝐵 ) )
7		elin	⊢ ( 𝑤 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ↔ ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑤 ∈ 𝐵 ) )
8	7	notbii	⊢ ( ¬ 𝑤 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ↔ ¬ ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑤 ∈ 𝐵 ) )
9		pm4.62	⊢ ( ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ¬ 𝑤 ∈ 𝐵 ) ↔ ( ¬ 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∨ ¬ 𝑤 ∈ 𝐵 ) )
10	6 8 9	3bitr4i	⊢ ( ¬ 𝑤 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ↔ ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ¬ 𝑤 ∈ 𝐵 ) )
11	10	biimpi	⊢ ( ¬ 𝑤 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) → ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ¬ 𝑤 ∈ 𝐵 ) )
12	11	impcom	⊢ ( ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ ¬ 𝑤 ∈ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ) → ¬ 𝑤 ∈ 𝐵 )
13	5 12	sylan2b	⊢ ( ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ ¬ 𝑤 ∈ 𝐶 ) → ¬ 𝑤 ∈ 𝐵 )
14	13	ex	⊢ ( 𝑤 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( ¬ 𝑤 ∈ 𝐶 → ¬ 𝑤 ∈ 𝐵 ) )
15	3 14	syl6	⊢ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ( ¬ 𝑤 ∈ 𝐶 → ¬ 𝑤 ∈ 𝐵 ) ) )
16	15	a2d	⊢ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) )
17	16	biantru	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ↔ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
18		df-3an	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ↔ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
19		3anass	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ↔ ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) )
20	17 18 19	3bitr2i	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ↔ ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) )
21	20	imbi2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) ) )
22	21	albii	⊢ ( ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ) ↔ ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) ) )
23	22	exbii	⊢ ( ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ) ↔ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) ) )
24	2 23	mpbi	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) )
25		imdi	⊢ ( ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ↔ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) → ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) )
26		pm3.35	⊢ ( ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) → ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) → ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) )
27	25 26	sylan2b	⊢ ( ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) → ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) )
28	27	anim2i	⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) )
29	28	imim2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) ) → ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
30	29	alimi	⊢ ( ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ∧ ( 𝜃 → ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) ) → ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
31	24 30	bnj101	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) )
32		ancl	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) → ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ) )
33		bnj256	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
34	32 33	imbitrrdi	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) → ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
35	34	alimi	⊢ ( ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) → ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
36	31 35	bnj101	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) )
37		df-bnj17	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) )
38	37	imbi2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
39	38	albii	⊢ ( ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ↔ ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
40	39	exbii	⊢ ( ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) ↔ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) ) )
41	36 40	mpbi	⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐵 ) ) ) )