Theorem dnnumch3 38112

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

Hypotheses

Ref	Expression
dnnumch.f	⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))
dnnumch.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
dnnumch.g	⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))

Assertion

Ref	Expression
dnnumch3	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On)

Distinct variable groups:   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦,𝑧   𝑥,𝐴,𝑦,𝑧   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦,𝑧)   𝐹(𝑧)   𝑉(𝑥,𝑦,𝑧)

Proof of Theorem dnnumch3

Dummy variables 𝑣 𝑤 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2156   ≠ wne 2978  ∀wral 3096  Vcvv 3391   ∖ cdif 3766   ⊆ wss 3769  ∅c0 4116  𝒫 cpw 4351  {csn 4370  ∩ cint 4669   ↦ cmpt 4923  ^◡ccnv 5310  dom cdm 5311  ran crn 5312   “ cima 5314  Oncon0 5936   Fn wfn 6092  ⟶wf 6093  –1-1→wf1 6094  ‘cfv 6097  recscrecs 7699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-wrecs 7638  df-recs 7700

This theorem is referenced by:  dnwech  38113