Metamath Proof Explorer

Theorem bnj1189

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 bnj1189.1 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) )
bnj1189.2 ⊢ ( 𝜓 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) )
bnj1189.3 ⊢ ( 𝜒 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
Assertion bnj1189 ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )

Proof

Step Hyp Ref Expression
1 bnj1189.1 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅ ) )
2 bnj1189.2 ⊢ ( 𝜓 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) )
3 bnj1189.3 ⊢ ( 𝜒 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
4 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 )
5 4 biimpi ⊢ ( 𝐵 ≠ ∅ → ∃ 𝑥 𝑥 ∈ 𝐵 )
6 1 5 bnj837 ⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐵 )
7 6 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ) )
8 19.42v ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ↔ ( 𝜑 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ) )
9 7 8 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) )
10 3simpc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝜒 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) )
11 3 anbi2i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝜒 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
12 10 11 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝜒 ) → ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
13 12 19.8ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝜒 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
14 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
15 13 14 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝜒 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
16 15 3comr ⊢ ( ( 𝜒 ∧ 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
17 16 3expib ⊢ ( 𝜒 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
18 simp1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → 𝜑 )
19 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → 𝑥 ∈ 𝐵 )
20 rexnal ⊢ ( ∃ 𝑦 ∈ 𝐵 ¬ ¬ 𝑦 𝑅 𝑥 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
21 20 bicomi ⊢ ( ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 ¬ ¬ 𝑦 𝑅 𝑥 )
22 21 3 xchnxbir ⊢ ( ¬ 𝜒 ↔ ∃ 𝑦 ∈ 𝐵 ¬ ¬ 𝑦 𝑅 𝑥 )
23 notnotb ⊢ ( 𝑦 𝑅 𝑥 ↔ ¬ ¬ 𝑦 𝑅 𝑥 )
24 23 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 ¬ ¬ 𝑦 𝑅 𝑥 )
25 22 24 bitr4i ⊢ ( ¬ 𝜒 ↔ ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑥 )
26 25 biimpi ⊢ ( ¬ 𝜒 → ∃ 𝑦 ∈ 𝐵 𝑦 𝑅 𝑥 )
27 26 bnj1196 ⊢ ( ¬ 𝜒 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) )
28 27 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) )
29 3anass ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) )
30 29 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) )
31 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) )
32 30 31 bitri ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) ) )
33 19 28 32 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝑅 𝑥 ) )
34 33 2 bnj1198 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → ∃ 𝑦 𝜓 )
35 19.42v ⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑦 𝜓 ) )
36 18 34 35 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) )
37 1 2 bnj1190 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑤 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑤 )
38 36 37 bnj593 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → ∃ 𝑦 ∃ 𝑤 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑤 )
39 38 bnj937 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → ∃ 𝑤 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 𝑅 𝑤 )
40 39 bnj1185 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ¬ 𝜒 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
41 40 3comr ⊢ ( ( ¬ 𝜒 ∧ 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
42 41 3expib ⊢ ( ¬ 𝜒 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ) )
43 17 42 pm2.61i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
44 9 43 bnj593 ⊢ ( 𝜑 → ∃ 𝑥 ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
45 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥
46 45 19.9 ⊢ ( ∃ 𝑥 ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )
47 44 46 sylib ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 𝑅 𝑥 )