Theorem bnj1176 32698

Description: Technical lemma for bnj69 32703. 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 3066	. . . . . . . . 9 ⊢ (∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧 ↔ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
5	4	rexbii 3170	. . . . . . . 8 ⊢ (∃𝑧 ∈ 𝐶 ∀𝑤 ∈ 𝐶 ¬ 𝑤𝑅𝑧 ↔ ∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
6	3, 5	sylib 221	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))
7		df-rex 3067	. . . . . . 7 ⊢ (∃𝑧 ∈ 𝐶 ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
8	6, 7	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
9		19.28v 1999	. . . . . . 7 ⊢ (∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
10	9	exbii 1855	. . . . . 6 ⊢ (∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ ∃𝑧(𝑧 ∈ 𝐶 ∧ ∀𝑤(𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
11	8, 10	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
12		19.37v 2000	. . . . 5 ⊢ (∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → ∃𝑧∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
13	11, 12	mpbir 234	. . . 4 ⊢ ∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
14		19.21v 1947	. . . . 5 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
15	14	exbii 1855	. . . 4 ⊢ (∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧((𝜑 ∧ 𝜓) → ∀𝑤(𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))))
16	13, 15	mpbir 234	. . 3 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)))
17		con2b 363	. . . . . . 7 ⊢ ((𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧) ↔ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))
18	17	anbi2i 626	. . . . . 6 ⊢ ((𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧)) ↔ (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
19	18	imbi2i 339	. . . . 5 ⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
20	19	albii 1827	. . . 4 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
21	20	exbii 1855	. . 3 ⊢ (∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤 ∈ 𝐶 → ¬ 𝑤𝑅𝑧))) ↔ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
22	16, 21	mpbi 233	. 2 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
23		ax-1 6	. . . . 5 ⊢ ((𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶) → (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))
24	23	anim2i 620	. . . 4 ⊢ ((𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))
25	24	imim2i 16	. . 3 ⊢ (((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) → ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))))
26	25	alimi 1819	. 2 ⊢ (∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))) → ∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶)))))
27	22, 26	bnj101 32414	1 ⊢ ∃𝑧∀𝑤((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝐶 ∧ (𝜃 → (𝑤𝑅𝑧 → ¬ 𝑤 ∈ 𝐶))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  ∀wal 1541  ∃wex 1787   ∈ wcel 2110   ≠ wne 2940  ∀wral 3061  ∃wrex 3062  Vcvv 3408   ⊆ wss 3866  ∅c0 4237   class class class wbr 5053   Fr wfr 5506   ∧ w-bnj17 32377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067

This theorem is referenced by:  bnj1190  32701