Theorem bnj1176 30327

Description: Technical lemma for bnj69 30332. 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 2901	. . . . . . . . 9 ⊢ (∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧 ↔ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
5	4	rexbii 3023	. . . . . . . 8 ⊢ (∃𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧 ↔ ∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
6	3, 5	sylib 207	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
7		df-rex 2902	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
8	6, 7	sylib 207	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
9		19.28v 1896	. . . . . . 7 ⊢ (∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
10	9	exbii 1764	. . . . . 6 ⊢ (∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
11	8, 10	sylibr 223	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
12		19.37v 1897	. . . . 5 ⊢ (∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → ∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
13	11, 12	mpbir 220	. . . 4 ⊢ ∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
14		19.21v 1855	. . . . 5 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
15	14	exbii 1764	. . . 4 ⊢ (∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
16	13, 15	mpbir 220	. . 3 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
17		con2b 348	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧) ↔ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))
18	17	anbi2i 726	. . . . . 6 ⊢ ((𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
19	18	imbi2i 325	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
20	19	albii 1737	. . . 4 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
21	20	exbii 1764	. . 3 ⊢ (∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
22	16, 21	mpbi 219	. 2 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
23		ax-1 6	. . . . 5 ⊢ ((𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶) → (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
24	23	anim2i 591	. . . 4 ⊢ ((𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
25	24	imim2i 16	. . 3 ⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) → ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))))
26	25	alimi 1730	. 2 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) → ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))))
27	22, 26	bnj101 30043	1 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   Fr wfr 4994   ∧ w-bnj17 30005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  bnj1190  30330