Theorem disjsuc

Description: Disjoint range Cartesian product, special case. (Contributed by Peter Mazsa, 25-Aug-2023)

	Ref	Expression
Assertion	disjsuc	|- ( A e. V -> ( Disj ( R |X. ( `' _E |` suc A ) ) <-> ( Disj ( R |X. ( `' _E |` A ) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		disjsuc2	|- ( A e. V -> ( A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )
2		df-suc	|- suc A = ( A u. { A } )
3	2	reseq2i	|- ( `' _E |` suc A ) = ( `' _E |` ( A u. { A } ) )
4	3	xrneq2i	|- ( R |X. ( `' _E |` suc A ) ) = ( R |X. ( `' _E |` ( A u. { A } ) ) )
5	4	disjeqi	|- ( Disj ( R |X. ( `' _E |` suc A ) ) <-> Disj ( R |X. ( `' _E |` ( A u. { A } ) ) ) )
6		disjxrnres5	|- ( Disj ( R |X. ( `' _E |` ( A u. { A } ) ) ) <-> A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) )
7	5 6	bitri	|- ( Disj ( R |X. ( `' _E |` suc A ) ) <-> A. u e. ( A u. { A } ) A. v e. ( A u. { A } ) ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) )
8		disjxrnres5	|- ( Disj ( R |X. ( `' _E |` A ) ) <-> A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) )
9	8	anbi1i	|- ( ( Disj ( R |X. ( `' _E |` A ) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) <-> ( A. u e. A A. v e. A ( u = v \/ ( [ u ] ( R |X. `' _E ) i^i [ v ] ( R |X. `' _E ) ) = (/) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) )
10	1 7 9	3bitr4g	|- ( A e. V -> ( Disj ( R |X. ( `' _E |` suc A ) ) <-> ( Disj ( R |X. ( `' _E |` A ) ) /\ A. u e. A ( ( u i^i A ) = (/) \/ ( [ u ] R i^i [ A ] R ) = (/) ) ) ) )