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 ⊢φ∧ψ→RFrA∧C⊆A∧C≠∅∧C∈V
bnj1176.52 ⊢RFrA∧C⊆A∧C≠∅∧C∈V→∃z∈C∀w∈C¬wRz
Assertion bnj1176 ⊢∃z∀wφ∧ψ→z∈C∧θ→wRz→¬w∈C

Proof

Step Hyp Ref Expression
1 bnj1176.51 ⊢φ∧ψ→RFrA∧C⊆A∧C≠∅∧C∈V
2 bnj1176.52 ⊢RFrA∧C⊆A∧C≠∅∧C∈V→∃z∈C∀w∈C¬wRz
3 1 2 syl ⊢φ∧ψ→∃z∈C∀w∈C¬wRz
4 df-ral ⊢∀w∈C¬wRz↔∀ww∈C→¬wRz
5 4 rexbii ⊢∃z∈C∀w∈C¬wRz↔∃z∈C∀ww∈C→¬wRz
6 3 5 sylib ⊢φ∧ψ→∃z∈C∀ww∈C→¬wRz
7 df-rex ⊢∃z∈C∀ww∈C→¬wRz↔∃zz∈C∧∀ww∈C→¬wRz
8 6 7 sylib ⊢φ∧ψ→∃zz∈C∧∀ww∈C→¬wRz
9 19.28v ⊢∀wz∈C∧w∈C→¬wRz↔z∈C∧∀ww∈C→¬wRz
10 9 exbii ⊢∃z∀wz∈C∧w∈C→¬wRz↔∃zz∈C∧∀ww∈C→¬wRz
11 8 10 sylibr ⊢φ∧ψ→∃z∀wz∈C∧w∈C→¬wRz
12 19.37v ⊢∃zφ∧ψ→∀wz∈C∧w∈C→¬wRz↔φ∧ψ→∃z∀wz∈C∧w∈C→¬wRz
13 11 12 mpbir ⊢∃zφ∧ψ→∀wz∈C∧w∈C→¬wRz
14 19.21v ⊢∀wφ∧ψ→z∈C∧w∈C→¬wRz↔φ∧ψ→∀wz∈C∧w∈C→¬wRz
15 14 exbii ⊢∃z∀wφ∧ψ→z∈C∧w∈C→¬wRz↔∃zφ∧ψ→∀wz∈C∧w∈C→¬wRz
16 13 15 mpbir ⊢∃z∀wφ∧ψ→z∈C∧w∈C→¬wRz
17 con2b ⊢w∈C→¬wRz↔wRz→¬w∈C
18 17 anbi2i ⊢z∈C∧w∈C→¬wRz↔z∈C∧wRz→¬w∈C
19 18 imbi2i ⊢φ∧ψ→z∈C∧w∈C→¬wRz↔φ∧ψ→z∈C∧wRz→¬w∈C
20 19 albii ⊢∀wφ∧ψ→z∈C∧w∈C→¬wRz↔∀wφ∧ψ→z∈C∧wRz→¬w∈C
21 20 exbii ⊢∃z∀wφ∧ψ→z∈C∧w∈C→¬wRz↔∃z∀wφ∧ψ→z∈C∧wRz→¬w∈C
22 16 21 mpbi ⊢∃z∀wφ∧ψ→z∈C∧wRz→¬w∈C
23 ax-1 ⊢wRz→¬w∈C→θ→wRz→¬w∈C
24 23 anim2i ⊢z∈C∧wRz→¬w∈C→z∈C∧θ→wRz→¬w∈C
25 24 imim2i ⊢φ∧ψ→z∈C∧wRz→¬w∈C→φ∧ψ→z∈C∧θ→wRz→¬w∈C
26 25 alimi ⊢∀wφ∧ψ→z∈C∧wRz→¬w∈C→∀wφ∧ψ→z∈C∧θ→wRz→¬w∈C
27 22 26 bnj101 ⊢∃z∀wφ∧ψ→z∈C∧θ→wRz→¬w∈C