Metamath Proof Explorer

Theorem caofrss

Description: Transfer a relation subset law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses caofref.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
caofref.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
caofcom.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
caofrss.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑅 𝑦 → 𝑥 𝑇 𝑦 ) )
Assertion caofrss ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 → 𝐹 ∘r 𝑇 𝐺 ) )

Proof

Step Hyp Ref Expression
1 caofref.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 caofref.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3 caofcom.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
4 caofrss.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑅 𝑦 → 𝑥 𝑇 𝑦 ) )
5 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
6 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
7 4 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝑅 𝑦 → 𝑥 𝑇 𝑦 ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝑅 𝑦 → 𝑥 𝑇 𝑦 ) )
9 breq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) )
10 breq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑇 𝑦 ↔ ( 𝐹 ‘ 𝑤 ) 𝑇 𝑦 ) )
11 9 10 imbi12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑥 𝑅 𝑦 → 𝑥 𝑇 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 → ( 𝐹 ‘ 𝑤 ) 𝑇 𝑦 ) ) )
12 breq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) )
13 breq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑇 𝑦 ↔ ( 𝐹 ‘ 𝑤 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) )
14 12 13 imbi12d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 → ( 𝐹 ‘ 𝑤 ) 𝑇 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑤 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) )
15 11 14 rspc2va ⊢ ( ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝑅 𝑦 → 𝑥 𝑇 𝑦 ) ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑤 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) )
16 5 6 8 15 syl21anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑤 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) )
17 16 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) → ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) )
18 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
19 3 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
20 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
21 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
22 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
23 18 19 1 1 20 21 22 ofrfval ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) )
24 18 19 1 1 20 21 22 ofrfval ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑇 𝐺 ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) )
25 17 23 24 3imtr4d ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 → 𝐹 ∘r 𝑇 𝐺 ) )