Theorem bnj1098

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

	Ref	Expression
Hypothesis	bnj1098.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
Assertion	bnj1098	⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1098.1	⊢ 𝐷 = ( ω ∖ { ∅ } )
2		3anrev	⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ∧ 𝑖 ≠ ∅ ) )
3		df-3an	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ∧ 𝑖 ≠ ∅ ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) ∧ 𝑖 ≠ ∅ ) )
4	2 3	bitri	⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) ∧ 𝑖 ≠ ∅ ) )
5		simpr	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) → 𝑖 ∈ 𝑛 )
6	1	bnj923	⊢ ( 𝑛 ∈ 𝐷 → 𝑛 ∈ ω )
7	6	adantr	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) → 𝑛 ∈ ω )
8		elnn	⊢ ( ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ ω ) → 𝑖 ∈ ω )
9	5 7 8	syl2anc	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) → 𝑖 ∈ ω )
10	9	anim1i	⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) ∧ 𝑖 ≠ ∅ ) → ( 𝑖 ∈ ω ∧ 𝑖 ≠ ∅ ) )
11	4 10	sylbi	⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑖 ∈ ω ∧ 𝑖 ≠ ∅ ) )
12		nnsuc	⊢ ( ( 𝑖 ∈ ω ∧ 𝑖 ≠ ∅ ) → ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 )
13	11 12	syl	⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 )
14		df-rex	⊢ ( ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ↔ ∃ 𝑗 ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) )
15	14	imbi2i	⊢ ( ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) ↔ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑗 ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ) )
16		19.37v	⊢ ( ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ) ↔ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑗 ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ) )
17	15 16	bitr4i	⊢ ( ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ∃ 𝑗 ∈ ω 𝑖 = suc 𝑗 ) ↔ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ) )
18	13 17	mpbi	⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) )
19		ancr	⊢ ( ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ) → ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) ) )
20	18 19	bnj101	⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) )
21		vex	⊢ 𝑗 ∈ V
22	21	bnj216	⊢ ( 𝑖 = suc 𝑗 → 𝑗 ∈ 𝑖 )
23	22	ad2antlr	⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) → 𝑗 ∈ 𝑖 )
24		simpr2	⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) → 𝑖 ∈ 𝑛 )
25		3simpc	⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) )
26	25	ancomd	⊢ ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) )
27	26	adantl	⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) → ( 𝑛 ∈ 𝐷 ∧ 𝑖 ∈ 𝑛 ) )
28		nnord	⊢ ( 𝑛 ∈ ω → Ord 𝑛 )
29		ordtr1	⊢ ( Ord 𝑛 → ( ( 𝑗 ∈ 𝑖 ∧ 𝑖 ∈ 𝑛 ) → 𝑗 ∈ 𝑛 ) )
30	27 7 28 29	4syl	⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) → ( ( 𝑗 ∈ 𝑖 ∧ 𝑖 ∈ 𝑛 ) → 𝑗 ∈ 𝑛 ) )
31	23 24 30	mp2and	⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) → 𝑗 ∈ 𝑛 )
32		simplr	⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) → 𝑖 = suc 𝑗 )
33	31 32	jca	⊢ ( ( ( 𝑗 ∈ ω ∧ 𝑖 = suc 𝑗 ) ∧ ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) )
34	20 33	bnj1023	⊢ ∃ 𝑗 ( ( 𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ) )