Theorem bnj1190

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	bnj1190.1	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) )
	bnj1190.2	⊢ ( 𝜓 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) )
Assertion	bnj1190	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑤 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑤 )

Proof

Step	Hyp	Ref	Expression
1		bnj1190.1	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) )
2		bnj1190.2	⊢ ( 𝜓 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) )
3	1	simp2bi	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐵 ⊆ 𝐴 )
5		eqid	⊢ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) = ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 )
6	1	simp1bi	⊢ ( 𝜑 → 𝑅 FrSe 𝐴 )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑅 FrSe 𝐴 )
8	2	simp1bi	⊢ ( 𝜓 → 𝑥 ∈ 𝐵 )
9		ssel2	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
10	3 8 9	syl2an	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 ∈ 𝐴 )
11	2 5 7 4 10	bnj1177	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 Fr 𝐴 ∧ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ⊆ 𝐴 ∧ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ≠ ∅ ∧ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ∈ V ) )
12		bnj1154	⊢ ( ( 𝑅 Fr 𝐴 ∧ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ⊆ 𝐴 ∧ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ≠ ∅ ∧ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ∈ V ) → ∃ 𝑢 ∈ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ∀ 𝑣 ∈ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ¬ 𝑣 𝑅 𝑢 )
13	11 12	bnj1176	⊢ ∃ 𝑢 ∀ 𝑣 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑢 ∈ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ∧ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝑣 𝑅 𝑢 → ¬ 𝑣 ∈ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ) ) ) )
14		biid	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 𝑅 𝑢 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑣 𝑅 𝑢 ) ) )
15		biid	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) )
16	5 14 15	bnj1175	⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝑣 𝑅 𝑢 → 𝑣 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
17	5 13 16	bnj1174	⊢ ∃ 𝑢 ∀ 𝑣 ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ∧ 𝑢 ∈ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ) ∧ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝑣 𝑅 𝑢 → ¬ 𝑣 ∈ 𝐵 ) ) ) )
18	5 15 7 10	bnj1173	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝑢 ∈ ( trCl ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐵 ) ) → ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑢 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ ( 𝑅 FrSe 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) ↔ 𝑣 ∈ 𝐴 ) )
19	5 17 18	bnj1172	⊢ ∃ 𝑢 ∀ 𝑣 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑢 ∈ 𝐵 ∧ ( 𝑣 ∈ 𝐴 → ( 𝑣 𝑅 𝑢 → ¬ 𝑣 ∈ 𝐵 ) ) ) )
20	4 19	bnj1171	⊢ ∃ 𝑢 ∀ 𝑣 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑢 ∈ 𝐵 ∧ ( 𝑣 ∈ 𝐵 → ¬ 𝑣 𝑅 𝑢 ) ) )
21	20	bnj1186	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑢 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ¬ 𝑣 𝑅 𝑢 )
22	21	bnj1185	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
23	22	bnj1185	⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑤 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑤 )