This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) = (/) ) ) ) )