Theorem disjf1o

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

	Ref	Expression
Hypotheses	disjf1o.xph	⊢ Ⅎ 𝑥 𝜑
	disjf1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	disjf1o.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	disjf1o.dj	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
	disjf1o.d	⊢ 𝐶 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ }
	disjf1o.e	⊢ 𝐷 = ( ran 𝐹 ∖ { ∅ } )
Assertion	disjf1o	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		disjf1o.xph	⊢ Ⅎ 𝑥 𝜑
2		disjf1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3		disjf1o.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4		disjf1o.dj	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
5		disjf1o.d	⊢ 𝐶 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ }
6		disjf1o.e	⊢ 𝐷 = ( ran 𝐹 ∖ { ∅ } )
7		eqid	⊢ ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 )
8		simpl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝜑 )
9		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ⊆ 𝐴
10	5 9	eqsstri	⊢ 𝐶 ⊆ 𝐴
11		id	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐶 )
12	10 11	sseldi	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐴 )
14	8 13 3	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ∈ 𝑉 )
15	11 5	eleqtrdi	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } )
16		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) )
17	16	a1i	⊢ ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ) )
18	15 17	mpbid	⊢ ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) )
19	18	simprd	⊢ ( 𝑥 ∈ 𝐶 → 𝐵 ≠ ∅ )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐵 ≠ ∅ )
21	10	a1i	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
22		disjss1	⊢ ( 𝐶 ⊆ 𝐴 → ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ 𝐶 𝐵 ) )
23	21 4 22	sylc	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐶 𝐵 )
24	1 7 14 20 23	disjf1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) : 𝐶 –1-1→ 𝑉 )
25		f1f1orn	⊢ ( ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) : 𝐶 –1-1→ 𝑉 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) : 𝐶 –1-1-onto→ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
26	24 25	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) : 𝐶 –1-1-onto→ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
27	2	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
28	27	reseq1d	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) )
29	21	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
30	28 29	eqtrd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
31		eqidd	⊢ ( 𝜑 → 𝐶 = 𝐶 )
32		simpl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 )
33		id	⊢ ( 𝑦 ∈ 𝐷 → 𝑦 ∈ 𝐷 )
34	33 6	eleqtrdi	⊢ ( 𝑦 ∈ 𝐷 → 𝑦 ∈ ( ran 𝐹 ∖ { ∅ } ) )
35		eldifsni	⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { ∅ } ) → 𝑦 ≠ ∅ )
36	34 35	syl	⊢ ( 𝑦 ∈ 𝐷 → 𝑦 ≠ ∅ )
37	36	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ≠ ∅ )
38		eldifi	⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { ∅ } ) → 𝑦 ∈ ran 𝐹 )
39	34 38	syl	⊢ ( 𝑦 ∈ 𝐷 → 𝑦 ∈ ran 𝐹 )
40	2	elrnmpt	⊢ ( 𝑦 ∈ ran 𝐹 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
41	39 40	syl	⊢ ( 𝑦 ∈ 𝐷 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) )
42	39 41	mpbid	⊢ ( 𝑦 ∈ 𝐷 → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
44		nfv	⊢ Ⅎ 𝑥 𝑦 ≠ ∅
45	1 44	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ≠ ∅ )
46		nfcv	⊢ Ⅎ 𝑥 𝑦
47		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐶 ↦ 𝐵 )
48	47	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 )
49	46 48	nfel	⊢ Ⅎ 𝑥 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 )
50		simp3	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
51		simp2	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝐴 )
52		id	⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
53	52	eqcomd	⊢ ( 𝑦 = 𝐵 → 𝐵 = 𝑦 )
54	53	adantl	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑦 = 𝐵 ) → 𝐵 = 𝑦 )
55		simpl	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑦 = 𝐵 ) → 𝑦 ≠ ∅ )
56	54 55	eqnetrd	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑦 = 𝐵 ) → 𝐵 ≠ ∅ )
57	56	3adant2	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐵 ≠ ∅ )
58	51 57	jca	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) )
59	58 16	sylibr	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } )
60	5	eqcomi	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } = 𝐶
61	60	a1i	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ ∅ } = 𝐶 )
62	59 61	eleqtrd	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝐶 )
63		eqvisset	⊢ ( 𝑦 = 𝐵 → 𝐵 ∈ V )
64	63	3ad2ant3	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐵 ∈ V )
65	7	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝐵 ∈ V ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
66	62 64 65	syl2anc	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
67	50 66	eqeltrd	⊢ ( ( 𝑦 ≠ ∅ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
68	67	3adant1l	⊢ ( ( ( 𝜑 ∧ 𝑦 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
69	68	3exp	⊢ ( ( 𝜑 ∧ 𝑦 ≠ ∅ ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 = 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) ) )
70	45 49 69	rexlimd	⊢ ( ( 𝜑 ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 → 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) )
71	70	imp	⊢ ( ( ( 𝜑 ∧ 𝑦 ≠ ∅ ) ∧ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
72	32 37 43 71	syl21anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
73	72	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐷 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
74		dfss3	⊢ ( 𝐷 ⊆ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐷 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
75	73 74	sylibr	⊢ ( 𝜑 → 𝐷 ⊆ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
76		simpl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) → 𝜑 )
77		vex	⊢ 𝑦 ∈ V
78	7	elrnmpt	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 ) )
79	77 78	ax-mp	⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 )
80	79	biimpi	⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 )
81	80	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 )
82		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐷
83		simpr	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
84	12	adantr	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝐴 )
85	83 63	syl	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝐵 ∈ V )
86	2	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) → 𝐵 ∈ ran 𝐹 )
87	84 85 86	syl2anc	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝐵 ∈ ran 𝐹 )
88	83 87	eqeltrd	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝑦 ∈ ran 𝐹 )
89	88	3adant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝑦 ∈ ran 𝐹 )
90	19	adantr	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝐵 ≠ ∅ )
91	83 90	eqnetrd	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝑦 ≠ ∅ )
92		nelsn	⊢ ( 𝑦 ≠ ∅ → ¬ 𝑦 ∈ { ∅ } )
93	91 92	syl	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → ¬ 𝑦 ∈ { ∅ } )
94	93	3adant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → ¬ 𝑦 ∈ { ∅ } )
95	89 94	eldifd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝑦 ∈ ( ran 𝐹 ∖ { ∅ } ) )
96	95 6	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → 𝑦 ∈ 𝐷 )
97	96	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 → ( 𝑦 = 𝐵 → 𝑦 ∈ 𝐷 ) ) )
98	1 82 97	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 → 𝑦 ∈ 𝐷 ) )
99	98	imp	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐶 𝑦 = 𝐵 ) → 𝑦 ∈ 𝐷 )
100	76 81 99	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) → 𝑦 ∈ 𝐷 )
101	75 100	eqelssd	⊢ ( 𝜑 → 𝐷 = ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
102	30 31 101	f1oeq123d	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ 𝐷 ↔ ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) : 𝐶 –1-1-onto→ ran ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) )
103	26 102	mpbird	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1-onto→ 𝐷 )