Theorem bnj1176 31954

Description: Technical lemma for bnj69 31959. 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.)

Hypotheses

Ref	Expression
bnj1176.51	⊢ ((𝜑 ∧ 𝜓) → (𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V))
bnj1176.52	⊢ ((𝑅 Fr 𝐴 ∧ 𝐶 ⊆ 𝐴 ∧ 𝐶 ≠ ∅ ∧ 𝐶 ∈ V) → ∃𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧)

Assertion

Ref	Expression
bnj1176	⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))

Distinct variable groups:   𝑤,𝐶   𝜑,𝑤,𝑧   𝜓,𝑤,𝑧

Allowed substitution hints:   𝜃(𝑧,𝑤)   𝐴(𝑧,𝑤)   𝐶(𝑧)   𝑅(𝑧,𝑤)

Proof of Theorem bnj1176

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 387  ∀wal 1506  ∃wex 1743   ∈ wcel 2051   ≠ wne 2960  ∀wral 3081  ∃wrex 3082  Vcvv 3408   ⊆ wss 3822  ∅c0 4172   class class class wbr 4925   Fr wfr 5359   ∧ w-bnj17 31636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-ral 3086  df-rex 3087

This theorem is referenced by:  bnj1190  31957