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

Metamath Proof Explorer

Theorem bnj1176

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 bnj1176.51 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V ) )
bnj1176.52 ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V ) → ∃ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐶 ¬ 𝑤 𝑅 𝑧 )
Assertion bnj1176 ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 bnj1176.51 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V ) )
2 bnj1176.52 ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V ) → ∃ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐶 ¬ 𝑤 𝑅 𝑧 )
3 1 2 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐶 ¬ 𝑤 𝑅 𝑧 )
4 df-ral ⊢ ( ∀ 𝑤 ∈ 𝐶 ¬ 𝑤 𝑅 𝑧 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) )
5 4 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐶 ¬ 𝑤 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐶 ∀ 𝑤 ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) )
6 3 5 sylib ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝐶 ∀ 𝑤 ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) )
7 df-rex ⊢ ( ∃ 𝑧 ∈ 𝐶 ∀ 𝑤 ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) )
8 6 7 sylib ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) )
9 19.28v ⊢ ( ∀ 𝑤 ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ↔ ( 𝑧 ∈ 𝐶 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) )
10 9 exbii ⊢ ( ∃ 𝑧 ∀ 𝑤 ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ ∀ 𝑤 ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) )
11 8 10 sylibr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ∀ 𝑤 ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) )
12 19.37v ⊢ ( ∃ 𝑧 ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑤 ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ∀ 𝑤 ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) )
13 11 12 mpbir ⊢ ∃ 𝑧 ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑤 ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) )
14 19.21v ⊢ ( ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑤 ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) )
15 14 exbii ⊢ ( ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) ↔ ∃ 𝑧 ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑤 ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) )
16 13 15 mpbir ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) )
17 con2b ⊢ ( ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ↔ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) )
18 17 anbi2i ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ↔ ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) )
19 18 imbi2i ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) )
20 19 albii ⊢ ( ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) ↔ ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) )
21 20 exbii ⊢ ( ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 ∈ 𝐶 → ¬ 𝑤 𝑅 𝑧 ) ) ) ↔ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) )
22 16 21 mpbi ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) )
23 ax-1 ⊢ ( ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) → ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) )
24 23 anim2i ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) )
25 24 imim2i ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) → ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ) )
26 25 alimi ⊢ ( ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) → ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) ) )
27 22 26 bnj101 ⊢ ∃ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝐶 ∧ ( 𝜃 → ( 𝑤 𝑅 𝑧 → ¬ 𝑤 ∈ 𝐶 ) ) ) )