Theorem dnnumch3

Description: Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dnnumch.f	⊢ 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
2		dnnumch.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		dnnumch.g	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺 ‘ 𝑦 ) ∈ 𝑦 ) )
4		cnvimass	⊢ ( ◡ 𝐹 “ { 𝑥 } ) ⊆ dom 𝐹
5	1	tfr1	⊢ 𝐹 Fn On
6	5	fndmi	⊢ dom 𝐹 = On
7	4 6	sseqtri	⊢ ( ◡ 𝐹 “ { 𝑥 } ) ⊆ On
8	1 2 3	dnnumch2	⊢ ( 𝜑 → 𝐴 ⊆ ran 𝐹 )
9	8	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ran 𝐹 )
10		inisegn0	⊢ ( 𝑥 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑥 } ) ≠ ∅ )
11	9 10	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 𝑥 } ) ≠ ∅ )
12		oninton	⊢ ( ( ( ◡ 𝐹 “ { 𝑥 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑥 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑥 } ) ∈ On )
13	7 11 12	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∩ ( ◡ 𝐹 “ { 𝑥 } ) ∈ On )
14	13	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 ⟶ On )
15	1 2 3	dnnumch3lem	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
16	15	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ∩ ( ◡ 𝐹 “ { 𝑣 } ) )
17	1 2 3	dnnumch3lem	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
18	17	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) )
19	16 18	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) ↔ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) )
20		fveq2	⊢ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) )
21	20	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) )
22		cnvimass	⊢ ( ◡ 𝐹 “ { 𝑣 } ) ⊆ dom 𝐹
23	22 6	sseqtri	⊢ ( ◡ 𝐹 “ { 𝑣 } ) ⊆ On
24	8	sselda	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ ran 𝐹 )
25		inisegn0	⊢ ( 𝑣 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ )
26	24 25	sylib	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ )
27		onint	⊢ ( ( ( ◡ 𝐹 “ { 𝑣 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑣 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) )
28	23 26 27	sylancr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) )
29		fniniseg	⊢ ( 𝐹 Fn On → ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) ↔ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ On ∧ ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 ) ) )
30	5 29	ax-mp	⊢ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) ↔ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ On ∧ ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 ) )
31	30	simprbi	⊢ ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) ∈ ( ◡ 𝐹 “ { 𝑣 } ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 )
32	28 31	syl	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 )
33	32	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑣 } ) ) = 𝑣 )
35		cnvimass	⊢ ( ◡ 𝐹 “ { 𝑤 } ) ⊆ dom 𝐹
36	35 6	sseqtri	⊢ ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On
37	8	sselda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ran 𝐹 )
38		inisegn0	⊢ ( 𝑤 ∈ ran 𝐹 ↔ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
39	37 38	sylib	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ )
40		onint	⊢ ( ( ( ◡ 𝐹 “ { 𝑤 } ) ⊆ On ∧ ( ◡ 𝐹 “ { 𝑤 } ) ≠ ∅ ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
41	36 39 40	sylancr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) )
42		fniniseg	⊢ ( 𝐹 Fn On → ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ On ∧ ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 ) ) )
43	5 42	ax-mp	⊢ ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) ↔ ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ On ∧ ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 ) )
44	43	simprbi	⊢ ( ∩ ( ◡ 𝐹 “ { 𝑤 } ) ∈ ( ◡ 𝐹 “ { 𝑤 } ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 )
45	41 44	syl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 )
46	45	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 )
47	46	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) → ( 𝐹 ‘ ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) = 𝑤 )
48	21 34 47	3eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) ∧ ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) ) → 𝑣 = 𝑤 )
49	48	ex	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ∩ ( ◡ 𝐹 “ { 𝑣 } ) = ∩ ( ◡ 𝐹 “ { 𝑤 } ) → 𝑣 = 𝑤 ) )
50	19 49	sylbid	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
51	50	ralrimivva	⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
52		dff13	⊢ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 –1-1→ On ↔ ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 ⟶ On ∧ ∀ 𝑣 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑣 ) = ( ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) )
53	14 51 52	sylanbrc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ∩ ( ◡ 𝐹 “ { 𝑥 } ) ) : 𝐴 –1-1→ On )