Theorem disjlem17

Description: Lemma for disjdmqseq , partim2 and petlem via disjlem18 , (general version of the former prtlem17 ). (Contributed by Peter Mazsa, 10-Sep-2021)

	Ref	Expression
Assertion	disjlem17	⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( ∃ 𝑦 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑦 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) ↔ ∃ 𝑦 ( 𝑦 ∈ dom 𝑅 ∧ ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) ) )
2		an32	⊢ ( ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ↔ ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) )
3		disjlem14	⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) ) )
4		eleq2	⊢ ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑥 ] 𝑅 ↔ 𝐵 ∈ [ 𝑦 ] 𝑅 ) )
5	4	biimprd	⊢ ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) )
6	3 5	syl8	⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )
7	6	exp4a	⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝐴 ∈ [ 𝑥 ] 𝑅 → ( 𝐴 ∈ [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) ) )
8	7	impd	⊢ ( Disj 𝑅 → ( ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( 𝐴 ∈ [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )
9	2 8	biimtrrid	⊢ ( Disj 𝑅 → ( ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝐴 ∈ [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )
10	9	expd	⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( 𝑦 ∈ dom 𝑅 → ( 𝐴 ∈ [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) ) )
11	10	imp5a	⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( 𝑦 ∈ dom 𝑅 → ( ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )
12	11	imp4b	⊢ ( ( Disj 𝑅 ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( ( 𝑦 ∈ dom 𝑅 ∧ ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) )
13	12	exlimdv	⊢ ( ( Disj 𝑅 ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( ∃ 𝑦 ( 𝑦 ∈ dom 𝑅 ∧ ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) )
14	1 13	biimtrid	⊢ ( ( Disj 𝑅 ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( ∃ 𝑦 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) )
15	14	ex	⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( ∃ 𝑦 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) )