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 𝑛 ) ) → 𝑝 ∈ 𝐷 ) |