Theorem dnnumch3lem

Description: Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	dnnumch.f	⊢ 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
	dnnumch.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	dnnumch.g	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) )
Assertion	dnnumch3lem	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )

Proof

Step	Hyp	Ref	Expression
1		dnnumch.f	⊢ 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
2		dnnumch.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		dnnumch.g	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) = ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) )
5		sneq	⊢ ( 𝑥 = 𝑤 → { 𝑥 } = { 𝑤 } )
6	5	imaeq2d	⊢ ( 𝑥 = 𝑤 → ( ◡ 𝐹 “ { 𝑥 } ) = ( ◡ 𝐹 “ { 𝑤 } ) )
7	6	inteqd	⊢ ( 𝑥 = 𝑤 → ∩ ( ◡ 𝐹 “ { 𝑥 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ 𝐴 )
9		cnvimass	⊢ ( ◡ 𝐹 “ { 𝑤 } ) ⊆ dom 𝐹
10	1	tfr1	⊢ 𝐹 Fn On
11	10	fndmi	⊢ dom 𝐹 = On
12	9 11	sseqtri	⊢ ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On
13	1 2 3	dnnumch2	⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 )
14	13	sselda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ran 𝐹 )
15		inisegn0	⊢ ( 𝑤 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
16	14 15	sylib	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
17		oninton	⊢ ( ( ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ On )
18	12 16 17	sylancr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ On )
19	4 7 8 18	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )