Theorem disjdmqsss

Description: Lemma for disjdmqseq via disjdmqs . (Contributed by Peter Mazsa, 16-Sep-2021)

	Ref	Expression
Assertion	disjdmqsss	⊢ ( Disj 𝑅 → ( dom 𝑅 / 𝑅 ) ⊆ ( dom ≀ 𝑅 / ≀ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		disjrel	⊢ ( Disj 𝑅 → Rel 𝑅 )
2		releldmqs	⊢ ( 𝑣 ∈ V → ( Rel 𝑅 → ( 𝑣 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑢 ] 𝑅 ) ) )
3	2	elv	⊢ ( Rel 𝑅 → ( 𝑣 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑢 ] 𝑅 ) )
4	1 3	syl	⊢ ( Disj 𝑅 → ( 𝑣 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑢 ] 𝑅 ) )
5		disjlem19	⊢ ( 𝑥 ∈ V → ( Disj 𝑅 → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑥 ∈ [ 𝑢 ] 𝑅 ) → [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ) ) )
6	5	elv	⊢ ( Disj 𝑅 → ( ( 𝑢 ∈ dom 𝑅 ∧ 𝑥 ∈ [ 𝑢 ] 𝑅 ) → [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ) )
7	6	ralrimivv	⊢ ( Disj 𝑅 → ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 )
8		2r19.29	⊢ ( ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑢 ] 𝑅 ) → ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑢 ] 𝑅 ) )
9	8	ex	⊢ ( ∀ 𝑢 ∈ dom 𝑅 ∀ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 → ( ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑢 ] 𝑅 → ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑢 ] 𝑅 ) ) )
10	7 9	syl	⊢ ( Disj 𝑅 → ( ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑢 ] 𝑅 → ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑢 ] 𝑅 ) ) )
11	4 10	sylbid	⊢ ( Disj 𝑅 → ( 𝑣 ∈ ( dom 𝑅 / 𝑅 ) → ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑢 ] 𝑅 ) ) )
12		eqtr	⊢ ( ( 𝑣 = [ 𝑢 ] 𝑅 ∧ [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ) → 𝑣 = [ 𝑥 ] ≀ 𝑅 )
13	12	ancoms	⊢ ( ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑢 ] 𝑅 ) → 𝑣 = [ 𝑥 ] ≀ 𝑅 )
14	13	reximi	⊢ ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑢 ] 𝑅 ) → ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑥 ] ≀ 𝑅 )
15	14	reximi	⊢ ( ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑢 ] 𝑅 ) → ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑥 ] ≀ 𝑅 )
16	11 15	syl6	⊢ ( Disj 𝑅 → ( 𝑣 ∈ ( dom 𝑅 / 𝑅 ) → ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑥 ] ≀ 𝑅 ) )
17		releldmqscoss	⊢ ( 𝑣 ∈ V → ( Rel 𝑅 → ( 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑥 ] ≀ 𝑅 ) ) )
18	17	elv	⊢ ( Rel 𝑅 → ( 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑥 ] ≀ 𝑅 ) )
19	1 18	syl	⊢ ( Disj 𝑅 → ( 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝑣 = [ 𝑥 ] ≀ 𝑅 ) )
20	16 19	sylibrd	⊢ ( Disj 𝑅 → ( 𝑣 ∈ ( dom 𝑅 / 𝑅 ) → 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ) )
21	20	ssrdv	⊢ ( Disj 𝑅 → ( dom 𝑅 / 𝑅 ) ⊆ ( dom ≀ 𝑅 / ≀ 𝑅 ) )