Metamath Proof Explorer

Theorem mptrcllem

Description: Show two versions of a closure with reflexive properties are equal. (Contributed by RP, 19-Oct-2020)

Ref Expression
Hypotheses mptrcllem.ex1 ⊢ ( 𝑥 ∈ 𝑉 → ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∈ V )
mptrcllem.ex2 ⊢ ( 𝑥 ∈ 𝑉 → ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } ∈ V )
mptrcllem.hyp1 ⊢ ( 𝑥 ∈ 𝑉 → 𝜒 )
mptrcllem.hyp2 ⊢ ( 𝑥 ∈ 𝑉 → 𝜃 )
mptrcllem.hyp3 ⊢ ( 𝑥 ∈ 𝑉 → 𝜏 )
mptrcllem.sub1 ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } → ( 𝜑 ↔ 𝜒 ) )
mptrcllem.sub2 ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } → ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ↔ 𝜃 ) )
mptrcllem.sub3 ⊢ ( 𝑧 = ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } → ( 𝜓 ↔ 𝜏 ) )
Assertion mptrcllem ( 𝑥 ∈ 𝑉 ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ 𝑉 ↦ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } )

Proof

Step Hyp Ref Expression
1 mptrcllem.ex1 ⊢ ( 𝑥 ∈ 𝑉 → ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ∈ V )
2 mptrcllem.ex2 ⊢ ( 𝑥 ∈ 𝑉 → ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } ∈ V )
3 mptrcllem.hyp1 ⊢ ( 𝑥 ∈ 𝑉 → 𝜒 )
4 mptrcllem.hyp2 ⊢ ( 𝑥 ∈ 𝑉 → 𝜃 )
5 mptrcllem.hyp3 ⊢ ( 𝑥 ∈ 𝑉 → 𝜏 )
6 mptrcllem.sub1 ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } → ( 𝜑 ↔ 𝜒 ) )
7 mptrcllem.sub2 ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } → ( ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ↔ 𝜃 ) )
8 mptrcllem.sub3 ⊢ ( 𝑧 = ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } → ( 𝜓 ↔ 𝜏 ) )
9 6 7 anbi12d ⊢ ( 𝑦 = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } → ( ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ↔ ( 𝜒 ∧ 𝜃 ) ) )
10 id ⊢ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 → ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 )
11 10 unssad ⊢ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 → 𝑥 ⊆ 𝑧 )
12 11 adantr ⊢ ( ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) → 𝑥 ⊆ 𝑧 )
13 12 a1i ⊢ ( 𝑥 ∈ 𝑉 → ( ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) → 𝑥 ⊆ 𝑧 ) )
14 13 alrimiv ⊢ ( 𝑥 ∈ 𝑉 → ∀ 𝑧 ( ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) → 𝑥 ⊆ 𝑧 ) )
15 ssintab ⊢ ( 𝑥 ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } ↔ ∀ 𝑧 ( ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) → 𝑥 ⊆ 𝑧 ) )
16 14 15 sylibr ⊢ ( 𝑥 ∈ 𝑉 → 𝑥 ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } )
17 3 4 jca ⊢ ( 𝑥 ∈ 𝑉 → ( 𝜒 ∧ 𝜃 ) )
18 2 9 16 17 clublem ⊢ ( 𝑥 ∈ 𝑉 → ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ⊆ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } )
19 simpl ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → 𝑥 ⊆ 𝑦 )
20 dmss ⊢ ( 𝑥 ⊆ 𝑦 → dom 𝑥 ⊆ dom 𝑦 )
21 rnss ⊢ ( 𝑥 ⊆ 𝑦 → ran 𝑥 ⊆ ran 𝑦 )
22 20 21 jca ⊢ ( 𝑥 ⊆ 𝑦 → ( dom 𝑥 ⊆ dom 𝑦 ∧ ran 𝑥 ⊆ ran 𝑦 ) )
23 unss12 ⊢ ( ( dom 𝑥 ⊆ dom 𝑦 ∧ ran 𝑥 ⊆ ran 𝑦 ) → ( dom 𝑥 ∪ ran 𝑥 ) ⊆ ( dom 𝑦 ∪ ran 𝑦 ) )
24 ssres2 ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ⊆ ( dom 𝑦 ∪ ran 𝑦 ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) )
25 22 23 24 3syl ⊢ ( 𝑥 ⊆ 𝑦 → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) )
26 25 adantr ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) )
27 simprr ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 )
28 26 27 sstrd ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑦 )
29 19 28 jca ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( 𝑥 ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑦 ) )
30 29 a1i ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( 𝑥 ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑦 ) ) )
31 unss ⊢ ( ( 𝑥 ⊆ 𝑦 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑦 ) ↔ ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑦 )
32 30 31 syl6ib ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑦 ) )
33 32 alrimiv ⊢ ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑦 ) )
34 ssintab ⊢ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ↔ ∀ 𝑦 ( ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) → ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑦 ) )
35 33 34 sylibr ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } )
36 1 8 35 5 clublem ⊢ ( 𝑥 ∈ 𝑉 → ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } ⊆ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } )
37 18 36 eqssd ⊢ ( 𝑥 ∈ 𝑉 → ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } = ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } )
38 37 mpteq2ia ⊢ ( 𝑥 ∈ 𝑉 ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ ( 𝜑 ∧ ( I ↾ ( dom 𝑦 ∪ ran 𝑦 ) ) ⊆ 𝑦 ) ) } ) = ( 𝑥 ∈ 𝑉 ↦ ∩ { 𝑧 ∣ ( ( 𝑥 ∪ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ) ⊆ 𝑧 ∧ 𝜓 ) } )