This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1279

Description: Technical lemma for bnj60 . 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 bnj1279.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1279.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1279.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1279.4 ⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
bnj1279.5 ⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
bnj1279.6 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
bnj1279.7 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
Assertion bnj1279 ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) = ∅ )

Proof

Step Hyp Ref Expression
1 bnj1279.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1279.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1279.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1279.4 ⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5 bnj1279.5 ⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
6 bnj1279.6 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
7 bnj1279.7 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8 n0 ⊢ ( ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) )
9 elin ⊢ ( 𝑦 ∈ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ↔ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑦 ∈ 𝐸 ) )
10 9 exbii ⊢ ( ∃ 𝑦 𝑦 ∈ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ↔ ∃ 𝑦 ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑦 ∈ 𝐸 ) )
11 8 10 sylbb ⊢ ( ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ → ∃ 𝑦 ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑦 ∈ 𝐸 ) )
12 df-bnj14 ⊢ pred ( 𝑥 , 𝐴 , 𝑅 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 }
13 12 bnj1538 ⊢ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑦 𝑅 𝑥 )
14 13 anim1i ⊢ ( ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑦 ∈ 𝐸 ) → ( 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) )
15 11 14 bnj593 ⊢ ( ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ → ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) )
16 15 3ad2ant3 ⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) → ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) )
17 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐸
18 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥
19 nfv ⊢ Ⅎ 𝑦 ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅
20 17 18 19 nf3an ⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ )
21 20 nf5ri ⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) → ∀ 𝑦 ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) )
22 16 21 bnj1275 ⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) → ∃ 𝑦 ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) )
23 simp2 ⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) → 𝑦 𝑅 𝑥 )
24 simp12 ⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) → ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 )
25 simp3 ⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) → 𝑦 ∈ 𝐸 )
26 24 25 bnj1294 ⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) → ¬ 𝑦 𝑅 𝑥 )
27 22 23 26 bnj1304 ⊢ ¬ ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ )
28 27 bnj1224 ⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) → ¬ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ )
29 nne ⊢ ( ¬ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ↔ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) = ∅ )
30 28 29 sylib ⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) = ∅ )