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 𝑖 ∈ 𝑚 )