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

Metamath Proof Explorer

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 𝑗 ) )