bnj986

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	bnj986.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj986.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj986.15	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
Assertion	bnj986	⊢ ( 𝜒 → ∃ 𝑚 ∃ 𝑝 𝜏 )

Proof

Step	Hyp	Ref	Expression
1		bnj986.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
2		bnj986.10	⊢ 𝐷 = ( ω ∖ { ∅ } )
3		bnj986.15	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
4	2	bnj158	⊢ ( 𝑛 ∈ 𝐷 → ∃ 𝑚 ∈ ω 𝑛 = suc 𝑚 )
5	1 4	bnj769	⊢ ( 𝜒 → ∃ 𝑚 ∈ ω 𝑛 = suc 𝑚 )
6	5	bnj1196	⊢ ( 𝜒 → ∃ 𝑚 ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) )
7		vex	⊢ 𝑛 ∈ V
8	7	sucex	⊢ suc 𝑛 ∈ V
9	8	isseti	⊢ ∃ 𝑝 𝑝 = suc 𝑛
10	6 9	jctir	⊢ ( 𝜒 → ( ∃ 𝑚 ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ ∃ 𝑝 𝑝 = suc 𝑛 ) )
11		exdistr	⊢ ( ∃ 𝑚 ∃ 𝑝 ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ 𝑝 = suc 𝑛 ) ↔ ∃ 𝑚 ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ ∃ 𝑝 𝑝 = suc 𝑛 ) )
12		19.41v	⊢ ( ∃ 𝑚 ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ ∃ 𝑝 𝑝 = suc 𝑛 ) ↔ ( ∃ 𝑚 ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ ∃ 𝑝 𝑝 = suc 𝑛 ) )
13	11 12	bitr2i	⊢ ( ( ∃ 𝑚 ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ ∃ 𝑝 𝑝 = suc 𝑛 ) ↔ ∃ 𝑚 ∃ 𝑝 ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ 𝑝 = suc 𝑛 ) )
14	10 13	sylib	⊢ ( 𝜒 → ∃ 𝑚 ∃ 𝑝 ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ 𝑝 = suc 𝑛 ) )
15		df-3an	⊢ ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) ↔ ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ 𝑝 = suc 𝑛 ) )
16	3 15	bitri	⊢ ( 𝜏 ↔ ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ 𝑝 = suc 𝑛 ) )
17	16	2exbii	⊢ ( ∃ 𝑚 ∃ 𝑝 𝜏 ↔ ∃ 𝑚 ∃ 𝑝 ( ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ) ∧ 𝑝 = suc 𝑛 ) )
18	14 17	sylibr	⊢ ( 𝜒 → ∃ 𝑚 ∃ 𝑝 𝜏 )

Metamath Proof Explorer

Theorem bnj986

Proof