Metamath Proof Explorer


Theorem bnj970

Description: Technical lemma for bnj69 . 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 bnj970.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
bnj970.10 𝐷 = ( ω ∖ { ∅ } )
Assertion bnj970 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝑝𝐷 )

Proof

Step Hyp Ref Expression
1 bnj970.3 ( 𝜒 ↔ ( 𝑛𝐷𝑓 Fn 𝑛𝜑𝜓 ) )
2 bnj970.10 𝐷 = ( ω ∖ { ∅ } )
3 1 bnj1232 ( 𝜒𝑛𝐷 )
4 3 3ad2ant1 ( ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) → 𝑛𝐷 )
5 4 adantl ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝑛𝐷 )
6 simpr3 ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝑝 = suc 𝑛 )
7 2 bnj923 ( 𝑛𝐷𝑛 ∈ ω )
8 peano2 ( 𝑛 ∈ ω → suc 𝑛 ∈ ω )
9 eleq1 ( 𝑝 = suc 𝑛 → ( 𝑝 ∈ ω ↔ suc 𝑛 ∈ ω ) )
10 bianir ( ( suc 𝑛 ∈ ω ∧ ( 𝑝 ∈ ω ↔ suc 𝑛 ∈ ω ) ) → 𝑝 ∈ ω )
11 8 9 10 syl2an ( ( 𝑛 ∈ ω ∧ 𝑝 = suc 𝑛 ) → 𝑝 ∈ ω )
12 7 11 sylan ( ( 𝑛𝐷𝑝 = suc 𝑛 ) → 𝑝 ∈ ω )
13 df-suc suc 𝑛 = ( 𝑛 ∪ { 𝑛 } )
14 13 eqeq2i ( 𝑝 = suc 𝑛𝑝 = ( 𝑛 ∪ { 𝑛 } ) )
15 ssun2 { 𝑛 } ⊆ ( 𝑛 ∪ { 𝑛 } )
16 vex 𝑛 ∈ V
17 16 snnz { 𝑛 } ≠ ∅
18 ssn0 ( ( { 𝑛 } ⊆ ( 𝑛 ∪ { 𝑛 } ) ∧ { 𝑛 } ≠ ∅ ) → ( 𝑛 ∪ { 𝑛 } ) ≠ ∅ )
19 15 17 18 mp2an ( 𝑛 ∪ { 𝑛 } ) ≠ ∅
20 neeq1 ( 𝑝 = ( 𝑛 ∪ { 𝑛 } ) → ( 𝑝 ≠ ∅ ↔ ( 𝑛 ∪ { 𝑛 } ) ≠ ∅ ) )
21 19 20 mpbiri ( 𝑝 = ( 𝑛 ∪ { 𝑛 } ) → 𝑝 ≠ ∅ )
22 14 21 sylbi ( 𝑝 = suc 𝑛𝑝 ≠ ∅ )
23 22 adantl ( ( 𝑛𝐷𝑝 = suc 𝑛 ) → 𝑝 ≠ ∅ )
24 2 eleq2i ( 𝑝𝐷𝑝 ∈ ( ω ∖ { ∅ } ) )
25 eldifsn ( 𝑝 ∈ ( ω ∖ { ∅ } ) ↔ ( 𝑝 ∈ ω ∧ 𝑝 ≠ ∅ ) )
26 24 25 bitri ( 𝑝𝐷 ↔ ( 𝑝 ∈ ω ∧ 𝑝 ≠ ∅ ) )
27 12 23 26 sylanbrc ( ( 𝑛𝐷𝑝 = suc 𝑛 ) → 𝑝𝐷 )
28 5 6 27 syl2anc ( ( ( 𝑅 FrSe 𝐴𝑋𝐴 ) ∧ ( 𝜒𝑛 = suc 𝑚𝑝 = suc 𝑛 ) ) → 𝑝𝐷 )