Theorem disjf1o 39378

Description: A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypotheses

Ref	Expression
disjf1o.xph	|- F/ x ph
disjf1o.f	|- F = ( x e. A |-> B )
disjf1o.b	|- ( ( ph /\ x e. A ) -> B e. V )
disjf1o.dj	|- ( ph -> Disj x e. A B )
disjf1o.d	|- C = { x e. A | B =/= (/) }
disjf1o.e	|- D = ( ran F \ { (/) } )

Assertion

Ref	Expression
disjf1o	|- ( ph -> ( F |` C ) : C -1-1-onto-> D )

Distinct variable groups:   x, A   x, C   x, D   x, V

Allowed substitution hints:   ph( x)   B( x)   F( x)

Proof of Theorem disjf1o

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		disjf1o.xph	. . . 4 |- F/ x ph
2		eqid 2622	. . . 4 |- ( x e. C |-> B ) = ( x e. C |-> B )
3		simpl 473	. . . . 5 |- ( ( ph /\ x e. C ) -> ph )
4		disjf1o.d	. . . . . . . 8 |- C = { x e. A | B =/= (/) }
5		ssrab2 3687	. . . . . . . 8 |- { x e. A | B =/= (/) } C_ A
6	4, 5	eqsstri 3635	. . . . . . 7 |- C C_ A
7		id 22	. . . . . . 7 |- ( x e. C -> x e. C )
8	6, 7	sseldi 3601	. . . . . 6 |- ( x e. C -> x e. A )
9	8	adantl 482	. . . . 5 |- ( ( ph /\ x e. C ) -> x e. A )
10		disjf1o.b	. . . . 5 |- ( ( ph /\ x e. A ) -> B e. V )
11	3, 9, 10	syl2anc 693	. . . 4 |- ( ( ph /\ x e. C ) -> B e. V )
12	7, 4	syl6eleq 2711	. . . . . . 7 |- ( x e. C -> x e. { x e. A | B =/= (/) } )
13		rabid 3116	. . . . . . . 8 |- ( x e. { x e. A | B =/= (/) } <-> ( x e. A /\ B =/= (/) ) )
14	13	a1i 11	. . . . . . 7 |- ( x e. C -> ( x e. { x e. A | B =/= (/) } <-> ( x e. A /\ B =/= (/) ) ) )
15	12, 14	mpbid 222	. . . . . 6 |- ( x e. C -> ( x e. A /\ B =/= (/) ) )
16	15	simprd 479	. . . . 5 |- ( x e. C -> B =/= (/) )
17	16	adantl 482	. . . 4 |- ( ( ph /\ x e. C ) -> B =/= (/) )
18	6	a1i 11	. . . . 5 |- ( ph -> C C_ A )
19		disjf1o.dj	. . . . 5 |- ( ph -> Disj x e. A B )
20		disjss1 4626	. . . . 5 |- ( C C_ A -> (Disj x e. A B -> Disj x e. C B ) )
21	18, 19, 20	sylc 65	. . . 4 |- ( ph -> Disj x e. C B )
22	1, 2, 11, 17, 21	disjf1 39369	. . 3 |- ( ph -> ( x e. C |-> B ) : C -1-1-> V )
23		f1f1orn 6148	. . 3 |- ( ( x e. C |-> B ) : C -1-1-> V -> ( x e. C |-> B ) : C -1-1-onto-> ran ( x e. C |-> B ) )
24	22, 23	syl 17	. 2 |- ( ph -> ( x e. C |-> B ) : C -1-1-onto-> ran ( x e. C |-> B ) )
25		disjf1o.f	. . . . . 6 |- F = ( x e. A |-> B )
26	25	a1i 11	. . . . 5 |- ( ph -> F = ( x e. A |-> B ) )
27	26	reseq1d 5395	. . . 4 |- ( ph -> ( F |` C ) = ( ( x e. A |-> B ) |` C ) )
28	18	resmptd 5452	. . . 4 |- ( ph -> ( ( x e. A |-> B ) |` C ) = ( x e. C |-> B ) )
29	27, 28	eqtrd 2656	. . 3 |- ( ph -> ( F |` C ) = ( x e. C |-> B ) )
30		eqidd 2623	. . 3 |- ( ph -> C = C )
31		simpl 473	. . . . . . 7 |- ( ( ph /\ y e. D ) -> ph )
32		id 22	. . . . . . . . . 10 |- ( y e. D -> y e. D )
33		disjf1o.e	. . . . . . . . . 10 |- D = ( ran F \ { (/) } )
34	32, 33	syl6eleq 2711	. . . . . . . . 9 |- ( y e. D -> y e. ( ran F \ { (/) } ) )
35		eldifsni 4320	. . . . . . . . 9 |- ( y e. ( ran F \ { (/) } ) -> y =/= (/) )
36	34, 35	syl 17	. . . . . . . 8 |- ( y e. D -> y =/= (/) )
37	36	adantl 482	. . . . . . 7 |- ( ( ph /\ y e. D ) -> y =/= (/) )
38		eldifi 3732	. . . . . . . . . 10 |- ( y e. ( ran F \ { (/) } ) -> y e. ran F )
39	34, 38	syl 17	. . . . . . . . 9 |- ( y e. D -> y e. ran F )
40	25	elrnmpt 5372	. . . . . . . . . 10 |- ( y e. ran F -> ( y e. ran F <-> E. x e. A y = B ) )
41	39, 40	syl 17	. . . . . . . . 9 |- ( y e. D -> ( y e. ran F <-> E. x e. A y = B ) )
42	39, 41	mpbid 222	. . . . . . . 8 |- ( y e. D -> E. x e. A y = B )
43	42	adantl 482	. . . . . . 7 |- ( ( ph /\ y e. D ) -> E. x e. A y = B )
44		nfv 1843	. . . . . . . . . 10 |- F/ x y =/= (/)
45	1, 44	nfan 1828	. . . . . . . . 9 |- F/ x ( ph /\ y =/= (/) )
46		nfcv 2764	. . . . . . . . . 10 |- F/_ x y
47		nfmpt1 4747	. . . . . . . . . . 11 |- F/_ x ( x e. C |-> B )
48	47	nfrn 5368	. . . . . . . . . 10 |- F/_ x ran ( x e. C |-> B )
49	46, 48	nfel 2777	. . . . . . . . 9 |- F/ x y e. ran ( x e. C |-> B )
50		simp3 1063	. . . . . . . . . . . 12 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> y = B )
51		simp2 1062	. . . . . . . . . . . . . . . 16 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> x e. A )
52		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( y = B -> y = B )
53	52	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 |- ( y = B -> B = y )
54	53	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( y =/= (/) /\ y = B ) -> B = y )
55		simpl 473	. . . . . . . . . . . . . . . . . 18 |- ( ( y =/= (/) /\ y = B ) -> y =/= (/) )
56	54, 55	eqnetrd 2861	. . . . . . . . . . . . . . . . 17 |- ( ( y =/= (/) /\ y = B ) -> B =/= (/) )
57	56	3adant2 1080	. . . . . . . . . . . . . . . 16 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> B =/= (/) )
58	51, 57	jca 554	. . . . . . . . . . . . . . 15 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> ( x e. A /\ B =/= (/) ) )
59	58, 13	sylibr 224	. . . . . . . . . . . . . 14 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> x e. { x e. A | B =/= (/) } )
60	4	eqcomi 2631	. . . . . . . . . . . . . . 15 |- { x e. A | B =/= (/) } = C
61	60	a1i 11	. . . . . . . . . . . . . 14 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> { x e. A | B =/= (/) } = C )
62	59, 61	eleqtrd 2703	. . . . . . . . . . . . 13 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> x e. C )
63		eqvisset 3211	. . . . . . . . . . . . . 14 |- ( y = B -> B e. _V )
64	63	3ad2ant3 1084	. . . . . . . . . . . . 13 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> B e. _V )
65	2	elrnmpt1 5374	. . . . . . . . . . . . 13 |- ( ( x e. C /\ B e. _V ) -> B e. ran ( x e. C |-> B ) )
66	62, 64, 65	syl2anc 693	. . . . . . . . . . . 12 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> B e. ran ( x e. C |-> B ) )
67	50, 66	eqeltrd 2701	. . . . . . . . . . 11 |- ( ( y =/= (/) /\ x e. A /\ y = B ) -> y e. ran ( x e. C |-> B ) )
68	67	3adant1l 1318	. . . . . . . . . 10 |- ( ( ( ph /\ y =/= (/) ) /\ x e. A /\ y = B ) -> y e. ran ( x e. C |-> B ) )
69	68	3exp 1264	. . . . . . . . 9 |- ( ( ph /\ y =/= (/) ) -> ( x e. A -> ( y = B -> y e. ran ( x e. C |-> B ) ) ) )
70	45, 49, 69	rexlimd 3026	. . . . . . . 8 |- ( ( ph /\ y =/= (/) ) -> ( E. x e. A y = B -> y e. ran ( x e. C |-> B ) ) )
71	70	imp 445	. . . . . . 7 |- ( ( ( ph /\ y =/= (/) ) /\ E. x e. A y = B ) -> y e. ran ( x e. C |-> B ) )
72	31, 37, 43, 71	syl21anc 1325	. . . . . 6 |- ( ( ph /\ y e. D ) -> y e. ran ( x e. C |-> B ) )
73	72	ralrimiva 2966	. . . . 5 |- ( ph -> A. y e. D y e. ran ( x e. C |-> B ) )
74		dfss3 3592	. . . . 5 |- ( D C_ ran ( x e. C |-> B ) <-> A. y e. D y e. ran ( x e. C |-> B ) )
75	73, 74	sylibr 224	. . . 4 |- ( ph -> D C_ ran ( x e. C |-> B ) )
76		simpl 473	. . . . . . 7 |- ( ( ph /\ y e. ran ( x e. C |-> B ) ) -> ph )
77		vex 3203	. . . . . . . . . 10 |- y e. _V
78	2	elrnmpt 5372	. . . . . . . . . 10 |- ( y e. _V -> ( y e. ran ( x e. C |-> B ) <-> E. x e. C y = B ) )
79	77, 78	ax-mp 5	. . . . . . . . 9 |- ( y e. ran ( x e. C |-> B ) <-> E. x e. C y = B )
80	79	biimpi 206	. . . . . . . 8 |- ( y e. ran ( x e. C |-> B ) -> E. x e. C y = B )
81	80	adantl 482	. . . . . . 7 |- ( ( ph /\ y e. ran ( x e. C |-> B ) ) -> E. x e. C y = B )
82		nfv 1843	. . . . . . . . 9 |- F/ x y e. D
83		simpr 477	. . . . . . . . . . . . . 14 |- ( ( x e. C /\ y = B ) -> y = B )
84	8	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( x e. C /\ y = B ) -> x e. A )
85	83, 63	syl 17	. . . . . . . . . . . . . . 15 |- ( ( x e. C /\ y = B ) -> B e. _V )
86	25	elrnmpt1 5374	. . . . . . . . . . . . . . 15 |- ( ( x e. A /\ B e. _V ) -> B e. ran F )
87	84, 85, 86	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( x e. C /\ y = B ) -> B e. ran F )
88	83, 87	eqeltrd 2701	. . . . . . . . . . . . 13 |- ( ( x e. C /\ y = B ) -> y e. ran F )
89	88	3adant1 1079	. . . . . . . . . . . 12 |- ( ( ph /\ x e. C /\ y = B ) -> y e. ran F )
90	16	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( x e. C /\ y = B ) -> B =/= (/) )
91	83, 90	eqnetrd 2861	. . . . . . . . . . . . . 14 |- ( ( x e. C /\ y = B ) -> y =/= (/) )
92		nelsn 4212	. . . . . . . . . . . . . 14 |- ( y =/= (/) -> -. y e. { (/) } )
93	91, 92	syl 17	. . . . . . . . . . . . 13 |- ( ( x e. C /\ y = B ) -> -. y e. { (/) } )
94	93	3adant1 1079	. . . . . . . . . . . 12 |- ( ( ph /\ x e. C /\ y = B ) -> -. y e. { (/) } )
95	89, 94	eldifd 3585	. . . . . . . . . . 11 |- ( ( ph /\ x e. C /\ y = B ) -> y e. ( ran F \ { (/) } ) )
96	95, 33	syl6eleqr 2712	. . . . . . . . . 10 |- ( ( ph /\ x e. C /\ y = B ) -> y e. D )
97	96	3exp 1264	. . . . . . . . 9 |- ( ph -> ( x e. C -> ( y = B -> y e. D ) ) )
98	1, 82, 97	rexlimd 3026	. . . . . . . 8 |- ( ph -> ( E. x e. C y = B -> y e. D ) )
99	98	imp 445	. . . . . . 7 |- ( ( ph /\ E. x e. C y = B ) -> y e. D )
100	76, 81, 99	syl2anc 693	. . . . . 6 |- ( ( ph /\ y e. ran ( x e. C |-> B ) ) -> y e. D )
101	100	ralrimiva 2966	. . . . 5 |- ( ph -> A. y e. ran ( x e. C |-> B ) y e. D )
102		dfss3 3592	. . . . 5 |- ( ran ( x e. C |-> B ) C_ D <-> A. y e. ran ( x e. C |-> B ) y e. D )
103	101, 102	sylibr 224	. . . 4 |- ( ph -> ran ( x e. C |-> B ) C_ D )
104	75, 103	eqssd 3620	. . 3 |- ( ph -> D = ran ( x e. C |-> B ) )
105	29, 30, 104	f1oeq123d 6133	. 2 |- ( ph -> ( ( F |` C ) : C -1-1-onto-> D <-> ( x e. C |-> B ) : C -1-1-onto-> ran ( x e. C |-> B ) ) )
106	24, 105	mpbird 247	1 |- ( ph -> ( F |` C ) : C -1-1-onto-> D )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   F/wnf 1708   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   C_ wss 3574   (/)c0 3915   {csn 4177  Disj wdisj 4620   |-> cmpt 4729   ran crn 5115   |` cres 5116   -1-1->wf1 5885   -1-1-onto->wf1o 5887

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-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  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-rmo 2920  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-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  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-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896

This theorem is referenced by:  sge0fodjrnlem  40633