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

Metamath Proof Explorer

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 𝑅 / 𝑅 ) )