This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑤 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑤 )