Theorem disjdsct

Description: A disjoint collection is distinct, i.e. each set in this collection is different of all others, provided that it does not contain the empty set This can be expressed as "the converse of the mapping function is a function", or "the mapping function is single-rooted". (Cf. funcnv ) (Contributed by Thierry Arnoux, 28-Feb-2017)

	Ref	Expression
Hypotheses	disjdsct.0	$$⊢Ⅎx\phi$$
	disjdsct.1	$$⊢\underset{\_}{Ⅎ}xA$$
	disjdsct.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left(V\setminus \left\{\varnothing \right\}\right)$$
	disjdsct.3	$$⊢\phi \to \underset{x\in A}{Disj}B$$
Assertion	disjdsct	$$⊢\phi \to \mathrm{Fun}{\left(x\in A⟼B\right)}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		disjdsct.0	$$⊢Ⅎx\phi$$
2		disjdsct.1	$$⊢\underset{\_}{Ⅎ}xA$$
3		disjdsct.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left(V\setminus \left\{\varnothing \right\}\right)$$
4		disjdsct.3	$$⊢\phi \to \underset{x\in A}{Disj}B$$
5	2	disjorsf	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall i\in A\forall j\in A\left(i=j\vee ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)$$
6	4 5	sylib	$$⊢\phi \to \forall i\in A\forall j\in A\left(i=j\vee ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)$$
7	6	r19.21bi	$$⊢\left(\phi \wedge i\in A\right)\to \forall j\in A\left(i=j\vee ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)$$
8	7	r19.21bi	$$⊢\left(\left(\phi \wedge i\in A\right)\wedge j\in A\right)\to \left(i=j\vee ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)$$
9		simpr3	$$⊢\left(\phi \wedge \left(i\in A\wedge j\in A\wedge ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)\right)\to ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing$$
10		eldifsni	$$⊢B\in \left(V\setminus \left\{\varnothing \right\}\right)\to B\ne \varnothing$$
11	3 10	syl	$$⊢\left(\phi \wedge x\in A\right)\to B\ne \varnothing$$
12	11	sbimi	$$⊢\left[i/x\right]\left(\phi \wedge x\in A\right)\to \left[i/x\right]B\ne \varnothing$$
13		sban	$$⊢\left[i/x\right]\left(\phi \wedge x\in A\right)\leftrightarrow \left(\left[i/x\right]\phi \wedge \left[i/x\right]x\in A\right)$$
14	1	sbf	$$⊢\left[i/x\right]\phi \leftrightarrow \phi$$
15	2	clelsb1fw	$$⊢\left[i/x\right]x\in A\leftrightarrow i\in A$$
16	14 15	anbi12i	$$⊢\left(\left[i/x\right]\phi \wedge \left[i/x\right]x\in A\right)\leftrightarrow \left(\phi \wedge i\in A\right)$$
17	13 16	bitri	$$⊢\left[i/x\right]\left(\phi \wedge x\in A\right)\leftrightarrow \left(\phi \wedge i\in A\right)$$
18		sbsbc	$$⊢\left[i/x\right]B\ne \varnothing \leftrightarrow \underset{\dot{}}{[}i/x\underset{\dot{}}{]}B\ne \varnothing$$
19		sbcne12	$$⊢\underset{\dot{}}{[}i/x\underset{\dot{}}{]}B\ne \varnothing \leftrightarrow ⦋i/x⦌B\ne ⦋i/x⦌\varnothing$$
20		csb0	$$⊢⦋i/x⦌\varnothing =\varnothing$$
21	20	neeq2i	$$⊢⦋i/x⦌B\ne ⦋i/x⦌\varnothing \leftrightarrow ⦋i/x⦌B\ne \varnothing$$
22	18 19 21	3bitri	$$⊢\left[i/x\right]B\ne \varnothing \leftrightarrow ⦋i/x⦌B\ne \varnothing$$
23	12 17 22	3imtr3i	$$⊢\left(\phi \wedge i\in A\right)\to ⦋i/x⦌B\ne \varnothing$$
24	23	3ad2antr1	$$⊢\left(\phi \wedge \left(i\in A\wedge j\in A\wedge ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)\right)\to ⦋i/x⦌B\ne \varnothing$$
25		disj3	$$⊢⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \leftrightarrow ⦋i/x⦌B=⦋i/x⦌B\setminus ⦋j/x⦌B$$
26	25	biimpi	$$⊢⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \to ⦋i/x⦌B=⦋i/x⦌B\setminus ⦋j/x⦌B$$
27	26	neeq1d	$$⊢⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \to \left(⦋i/x⦌B\ne \varnothing \leftrightarrow ⦋i/x⦌B\setminus ⦋j/x⦌B\ne \varnothing \right)$$
28	27	biimpa	$$⊢\left(⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \wedge ⦋i/x⦌B\ne \varnothing \right)\to ⦋i/x⦌B\setminus ⦋j/x⦌B\ne \varnothing$$
29		difn0	$$⊢⦋i/x⦌B\setminus ⦋j/x⦌B\ne \varnothing \to ⦋i/x⦌B\ne ⦋j/x⦌B$$
30	28 29	syl	$$⊢\left(⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \wedge ⦋i/x⦌B\ne \varnothing \right)\to ⦋i/x⦌B\ne ⦋j/x⦌B$$
31	9 24 30	syl2anc	$$⊢\left(\phi \wedge \left(i\in A\wedge j\in A\wedge ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)\right)\to ⦋i/x⦌B\ne ⦋j/x⦌B$$
32	31	3anassrs	$$⊢\left(\left(\left(\phi \wedge i\in A\right)\wedge j\in A\right)\wedge ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)\to ⦋i/x⦌B\ne ⦋j/x⦌B$$
33	32	ex	$$⊢\left(\left(\phi \wedge i\in A\right)\wedge j\in A\right)\to \left(⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \to ⦋i/x⦌B\ne ⦋j/x⦌B\right)$$
34	33	orim2d	$$⊢\left(\left(\phi \wedge i\in A\right)\wedge j\in A\right)\to \left(\left(i=j\vee ⦋i/x⦌B\cap ⦋j/x⦌B=\varnothing \right)\to \left(i=j\vee ⦋i/x⦌B\ne ⦋j/x⦌B\right)\right)$$
35	8 34	mpd	$$⊢\left(\left(\phi \wedge i\in A\right)\wedge j\in A\right)\to \left(i=j\vee ⦋i/x⦌B\ne ⦋j/x⦌B\right)$$
36	35	ralrimiva	$$⊢\left(\phi \wedge i\in A\right)\to \forall j\in A\left(i=j\vee ⦋i/x⦌B\ne ⦋j/x⦌B\right)$$
37	36	ralrimiva	$$⊢\phi \to \forall i\in A\forall j\in A\left(i=j\vee ⦋i/x⦌B\ne ⦋j/x⦌B\right)$$
38		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)$$
39		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
40	1 2 38 39 3	funcnv4mpt	$$⊢\phi \to \left(\mathrm{Fun}{\left(x\in A⟼B\right)}^{-1}\leftrightarrow \forall i\in A\forall j\in A\left(i=j\vee ⦋i/x⦌B\ne ⦋j/x⦌B\right)\right)$$
41	37 40	mpbird	$$⊢\phi \to \mathrm{Fun}{\left(x\in A⟼B\right)}^{-1}$$