Theorem disjdmqscossss

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

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

Proof

Step	Hyp	Ref	Expression
1		disjrel	⊢ ( Disj 𝑅 → Rel 𝑅 )
2		releldmqscoss	⊢ ( 𝑣 ∈ 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		eqtr3	⊢ ( ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑥 ] ≀ 𝑅 ) → [ 𝑢 ] 𝑅 = 𝑣 )
13	12	reximi	⊢ ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑥 ] ≀ 𝑅 ) → ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = 𝑣 )
14	13	reximi	⊢ ( ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 ( [ 𝑢 ] 𝑅 = [ 𝑥 ] ≀ 𝑅 ∧ 𝑣 = [ 𝑥 ] ≀ 𝑅 ) → ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = 𝑣 )
15	11 14	syl6	⊢ ( Disj 𝑅 → ( 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) → ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = 𝑣 ) )
16		df-rex	⊢ ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = 𝑣 ↔ ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ [ 𝑢 ] 𝑅 = 𝑣 ) )
17		19.41v	⊢ ( ∃ 𝑥 ( 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ [ 𝑢 ] 𝑅 = 𝑣 ) ↔ ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ [ 𝑢 ] 𝑅 = 𝑣 ) )
18	16 17	bitri	⊢ ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = 𝑣 ↔ ( ∃ 𝑥 𝑥 ∈ [ 𝑢 ] 𝑅 ∧ [ 𝑢 ] 𝑅 = 𝑣 ) )
19	18	simprbi	⊢ ( ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = 𝑣 → [ 𝑢 ] 𝑅 = 𝑣 )
20	19	reximi	⊢ ( ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 [ 𝑢 ] 𝑅 = 𝑣 → ∃ 𝑢 ∈ dom 𝑅 [ 𝑢 ] 𝑅 = 𝑣 )
21	15 20	syl6	⊢ ( Disj 𝑅 → ( 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) → ∃ 𝑢 ∈ dom 𝑅 [ 𝑢 ] 𝑅 = 𝑣 ) )
22		eqcom	⊢ ( [ 𝑢 ] 𝑅 = 𝑣 ↔ 𝑣 = [ 𝑢 ] 𝑅 )
23	22	rexbii	⊢ ( ∃ 𝑢 ∈ dom 𝑅 [ 𝑢 ] 𝑅 = 𝑣 ↔ ∃ 𝑢 ∈ dom 𝑅 𝑣 = [ 𝑢 ] 𝑅 )
24	21 23	imbitrdi	⊢ ( Disj 𝑅 → ( 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) → ∃ 𝑢 ∈ dom 𝑅 𝑣 = [ 𝑢 ] 𝑅 ) )
25	24	ss2abdv	⊢ ( Disj 𝑅 → { 𝑣 ∣ 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) } ⊆ { 𝑣 ∣ ∃ 𝑢 ∈ dom 𝑅 𝑣 = [ 𝑢 ] 𝑅 } )
26		abid1	⊢ ( dom ≀ 𝑅 / ≀ 𝑅 ) = { 𝑣 ∣ 𝑣 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) }
27		df-qs	⊢ ( dom 𝑅 / 𝑅 ) = { 𝑣 ∣ ∃ 𝑢 ∈ dom 𝑅 𝑣 = [ 𝑢 ] 𝑅 }
28	25 26 27	3sstr4g	⊢ ( Disj 𝑅 → ( dom ≀ 𝑅 / ≀ 𝑅 ) ⊆ ( dom 𝑅 / 𝑅 ) )