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 𝑇 𝐺 ) )