Theorem dnnumch3 37617

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 5485	. . . . 5 ⊢ (◡𝐹 “ {𝑥}) ⊆ dom 𝐹
2		dnnumch.f	. . . . . . 7 ⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧))))
3	2	tfr1 7493	. . . . . 6 ⊢ 𝐹 Fn On
4		fndm 5990	. . . . . 6 ⊢ (𝐹 Fn On → dom 𝐹 = On)
5	3, 4	ax-mp 5	. . . . 5 ⊢ dom 𝐹 = On
6	1, 5	sseqtri 3637	. . . 4 ⊢ (◡𝐹 “ {𝑥}) ⊆ On
7		dnnumch.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
8		dnnumch.g	. . . . . . 7 ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦))
9	2, 7, 8	dnnumch2 37615	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ ran 𝐹)
10	9	sselda 3603	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran 𝐹)
11		inisegn0 5497	. . . . 5 ⊢ (𝑥 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑥}) ≠ ∅)
12	10, 11	sylib 208	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡𝐹 “ {𝑥}) ≠ ∅)
13		oninton 7000	. . . 4 ⊢ (((◡𝐹 “ {𝑥}) ⊆ On ∧ (◡𝐹 “ {𝑥}) ≠ ∅) → ∩ (◡𝐹 “ {𝑥}) ∈ On)
14	6, 12, 13	sylancr 695	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑥}) ∈ On)
15		eqid 2622	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})) = (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))
16	14, 15	fmptd 6385	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On)
17	2, 7, 8	dnnumch3lem 37616	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣}))
18	17	adantrr 753	. . . . 5 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣}))
19	2, 7, 8	dnnumch3lem 37616	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤}))
20	19	adantrl 752	. . . . 5 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤}))
21	18, 20	eqeq12d 2637	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ↔ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})))
22		fveq2 6191	. . . . . . 7 ⊢ (∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = (𝐹‘∩ (◡𝐹 “ {𝑤})))
23	22	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = (𝐹‘∩ (◡𝐹 “ {𝑤})))
24		cnvimass 5485	. . . . . . . . . . 11 ⊢ (◡𝐹 “ {𝑣}) ⊆ dom 𝐹
25	24, 5	sseqtri 3637	. . . . . . . . . 10 ⊢ (◡𝐹 “ {𝑣}) ⊆ On
26	9	sselda 3603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑣 ∈ ran 𝐹)
27		inisegn0 5497	. . . . . . . . . . 11 ⊢ (𝑣 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑣}) ≠ ∅)
28	26, 27	sylib 208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (◡𝐹 “ {𝑣}) ≠ ∅)
29		onint 6995	. . . . . . . . . 10 ⊢ (((◡𝐹 “ {𝑣}) ⊆ On ∧ (◡𝐹 “ {𝑣}) ≠ ∅) → ∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}))
30	25, 28, 29	sylancr 695	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}))
31		fniniseg 6338	. . . . . . . . . . 11 ⊢ (𝐹 Fn On → (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) ↔ (∩ (◡𝐹 “ {𝑣}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣)))
32	3, 31	ax-mp 5	. . . . . . . . . 10 ⊢ (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) ↔ (∩ (◡𝐹 “ {𝑣}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣))
33	32	simprbi 480	. . . . . . . . 9 ⊢ (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣)
34	30, 33	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣)
35	34	adantrr 753	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣)
36	35	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣)
37		cnvimass 5485	. . . . . . . . . . 11 ⊢ (◡𝐹 “ {𝑤}) ⊆ dom 𝐹
38	37, 5	sseqtri 3637	. . . . . . . . . 10 ⊢ (◡𝐹 “ {𝑤}) ⊆ On
39	9	sselda 3603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ran 𝐹)
40		inisegn0 5497	. . . . . . . . . . 11 ⊢ (𝑤 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑤}) ≠ ∅)
41	39, 40	sylib 208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (◡𝐹 “ {𝑤}) ≠ ∅)
42		onint 6995	. . . . . . . . . 10 ⊢ (((◡𝐹 “ {𝑤}) ⊆ On ∧ (◡𝐹 “ {𝑤}) ≠ ∅) → ∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}))
43	38, 41, 42	sylancr 695	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}))
44		fniniseg 6338	. . . . . . . . . . 11 ⊢ (𝐹 Fn On → (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) ↔ (∩ (◡𝐹 “ {𝑤}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤)))
45	3, 44	ax-mp 5	. . . . . . . . . 10 ⊢ (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) ↔ (∩ (◡𝐹 “ {𝑤}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤))
46	45	simprbi 480	. . . . . . . . 9 ⊢ (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤)
47	43, 46	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤)
48	47	adantrl 752	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤)
49	48	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤)
50	23, 36, 49	3eqtr3d 2664	. . . . 5 ⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → 𝑣 = 𝑤)
51	50	ex 450	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}) → 𝑣 = 𝑤))
52	21, 51	sylbid 230	. . 3 ⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤))
53	52	ralrimivva 2971	. 2 ⊢ (𝜑 → ∀𝑣 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤))
54		dff13 6512	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On ↔ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On ∧ ∀𝑣 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤)))
55	16, 53, 54	sylanbrc 698	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  Vcvv 3200   ∖ cdif 3571   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158  {csn 4177  ∩ cint 4475   ↦ cmpt 4729  ^◡ccnv 5113  dom cdm 5114  ran crn 5115   “ cima 5117  Oncon0 5723   Fn wfn 5883  ⟶wf 5884  –1-1→wf1 5885  ‘cfv 5888  recscrecs 7467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-wrecs 7407  df-recs 7468

This theorem is referenced by:  dnwech  37618