Theorem bnj1176 32985

Description: Technical lemma for bnj69 32990. 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 3069	. . . . . . . . 9 ⊢ (∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧 ↔ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
5	4	rexbii 3181	. . . . . . . 8 ⊢ (∃𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧 ↔ ∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
6	3, 5	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
7		df-rex 3070	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
8	6, 7	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
9		19.28v 1994	. . . . . . 7 ⊢ (∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
10	9	exbii 1850	. . . . . 6 ⊢ (∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
11	8, 10	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
12		19.37v 1995	. . . . 5 ⊢ (∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → ∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
13	11, 12	mpbir 230	. . . 4 ⊢ ∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
14		19.21v 1942	. . . . 5 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
15	14	exbii 1850	. . . 4 ⊢ (∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
16	13, 15	mpbir 230	. . 3 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
17		con2b 360	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧) ↔ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))
18	17	anbi2i 623	. . . . . 6 ⊢ ((𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
19	18	imbi2i 336	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
20	19	albii 1822	. . . 4 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
21	20	exbii 1850	. . 3 ⊢ (∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
22	16, 21	mpbi 229	. 2 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
23		ax-1 6	. . . . 5 ⊢ ((𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶) → (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
24	23	anim2i 617	. . . 4 ⊢ ((𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
25	24	imim2i 16	. . 3 ⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) → ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))))
26	25	alimi 1814	. 2 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) → ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))))
27	22, 26	bnj101 32702	1 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396  ∀wal 1537  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ⊆ wss 3887  ∅c0 4256   class class class wbr 5074   Fr wfr 5541   ∧ w-bnj17 32665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  bnj1190  32988