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

Metamath Proof Explorer

Theorem bnj563

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj563.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
bnj563.21 ⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
Assertion bnj563 ( ( 𝜂 ∧ 𝜌 ) → suc 𝑖 ∈ 𝑚 )

Proof

Step Hyp Ref Expression
1 bnj563.19 ⊢ ( 𝜂 ↔ ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
2 bnj563.21 ⊢ ( 𝜌 ↔ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
3 bnj312 ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ↔ ( 𝑛 = suc 𝑚 ∧ 𝑚 ∈ 𝐷 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) )
4 bnj252 ⊢ ( ( 𝑛 = suc 𝑚 ∧ 𝑚 ∈ 𝐷 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ↔ ( 𝑛 = suc 𝑚 ∧ ( 𝑚 ∈ 𝐷 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ) )
5 3 4 bitri ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ↔ ( 𝑛 = suc 𝑚 ∧ ( 𝑚 ∈ 𝐷 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) ) )
6 5 simplbi ⊢ ( ( 𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝 ) → 𝑛 = suc 𝑚 )
7 1 6 sylbi ⊢ ( 𝜂 → 𝑛 = suc 𝑚 )
8 2 simp2bi ⊢ ( 𝜌 → suc 𝑖 ∈ 𝑛 )
9 2 simp3bi ⊢ ( 𝜌 → 𝑚 ≠ suc 𝑖 )
10 8 9 jca ⊢ ( 𝜌 → ( suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) )
11 necom ⊢ ( 𝑚 ≠ suc 𝑖 ↔ suc 𝑖 ≠ 𝑚 )
12 eleq2 ⊢ ( 𝑛 = suc 𝑚 → ( suc 𝑖 ∈ 𝑛 ↔ suc 𝑖 ∈ suc 𝑚 ) )
13 12 biimpa ⊢ ( ( 𝑛 = suc 𝑚 ∧ suc 𝑖 ∈ 𝑛 ) → suc 𝑖 ∈ suc 𝑚 )
14 elsuci ⊢ ( suc 𝑖 ∈ suc 𝑚 → ( suc 𝑖 ∈ 𝑚 ∨ suc 𝑖 = 𝑚 ) )
15 orcom ⊢ ( ( suc 𝑖 = 𝑚 ∨ suc 𝑖 ∈ 𝑚 ) ↔ ( suc 𝑖 ∈ 𝑚 ∨ suc 𝑖 = 𝑚 ) )
16 neor ⊢ ( ( suc 𝑖 = 𝑚 ∨ suc 𝑖 ∈ 𝑚 ) ↔ ( suc 𝑖 ≠ 𝑚 → suc 𝑖 ∈ 𝑚 ) )
17 15 16 bitr3i ⊢ ( ( suc 𝑖 ∈ 𝑚 ∨ suc 𝑖 = 𝑚 ) ↔ ( suc 𝑖 ≠ 𝑚 → suc 𝑖 ∈ 𝑚 ) )
18 14 17 sylib ⊢ ( suc 𝑖 ∈ suc 𝑚 → ( suc 𝑖 ≠ 𝑚 → suc 𝑖 ∈ 𝑚 ) )
19 18 imp ⊢ ( ( suc 𝑖 ∈ suc 𝑚 ∧ suc 𝑖 ≠ 𝑚 ) → suc 𝑖 ∈ 𝑚 )
20 13 19 stoic3 ⊢ ( ( 𝑛 = suc 𝑚 ∧ suc 𝑖 ∈ 𝑛 ∧ suc 𝑖 ≠ 𝑚 ) → suc 𝑖 ∈ 𝑚 )
21 11 20 syl3an3b ⊢ ( ( 𝑛 = suc 𝑚 ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) → suc 𝑖 ∈ 𝑚 )
22 21 3expb ⊢ ( ( 𝑛 = suc 𝑚 ∧ ( suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖 ) ) → suc 𝑖 ∈ 𝑚 )
23 7 10 22 syl2an ⊢ ( ( 𝜂 ∧ 𝜌 ) → suc 𝑖 ∈ 𝑚 )