Metamath Proof Explorer

Theorem caoftrn

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

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

Proof

Step Hyp Ref Expression
1 caofref.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 caofref.2 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3 caofcom.3 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
4 caofass.4 ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝑆 )
5 caoftrn.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) → 𝑥 𝑈 𝑧 ) )
6 5 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) → 𝑥 𝑈 𝑧 ) )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) → 𝑥 𝑈 𝑧 ) )
8 2 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
9 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
10 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑤 ) ∈ 𝑆 )
11 breq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ) )
12 11 anbi1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) ) )
13 breq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( 𝑥 𝑈 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) 𝑈 𝑧 ) )
14 12 13 imbi12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑤 ) → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) → 𝑥 𝑈 𝑧 ) ↔ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) → ( 𝐹 ‘ 𝑤 ) 𝑈 𝑧 ) ) )
15 breq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) )
16 breq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( 𝑦 𝑇 𝑧 ↔ ( 𝐺 ‘ 𝑤 ) 𝑇 𝑧 ) )
17 15 16 anbi12d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 𝑧 ) ) )
18 17 imbi1d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑤 ) → ( ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) → ( 𝐹 ‘ 𝑤 ) 𝑈 𝑧 ) ↔ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 𝑧 ) → ( 𝐹 ‘ 𝑤 ) 𝑈 𝑧 ) ) )
19 breq2 ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑤 ) → ( ( 𝐺 ‘ 𝑤 ) 𝑇 𝑧 ↔ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) )
20 19 anbi2d ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) ) )
21 breq2 ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑈 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) 𝑈 ( 𝐻 ‘ 𝑤 ) ) )
22 20 21 imbi12d ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑤 ) → ( ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 𝑧 ) → ( 𝐹 ‘ 𝑤 ) 𝑈 𝑧 ) ↔ ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) 𝑈 ( 𝐻 ‘ 𝑤 ) ) ) )
23 14 18 22 rspc3v ⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐻 ‘ 𝑤 ) ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) → 𝑥 𝑈 𝑧 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) 𝑈 ( 𝐻 ‘ 𝑤 ) ) ) )
24 8 9 10 23 syl3anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑇 𝑧 ) → 𝑥 𝑈 𝑧 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) 𝑈 ( 𝐻 ‘ 𝑤 ) ) ) )
25 7 24 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) 𝑈 ( 𝐻 ‘ 𝑤 ) ) )
26 25 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) → ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑈 ( 𝐻 ‘ 𝑤 ) ) )
27 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
28 3 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
29 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
30 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
31 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) )
32 27 28 1 1 29 30 31 ofrfval ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑅 𝐺 ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) )
33 4 ffnd ⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
34 eqidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑤 ) = ( 𝐻 ‘ 𝑤 ) )
35 28 33 1 1 29 31 34 ofrfval ⊢ ( 𝜑 → ( 𝐺 ∘r 𝑇 𝐻 ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) )
36 32 35 anbi12d ⊢ ( 𝜑 → ( ( 𝐹 ∘r 𝑅 𝐺 ∧ 𝐺 ∘r 𝑇 𝐻 ) ↔ ( ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) ) )
37 r19.26 ⊢ ( ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) ↔ ( ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) )
38 36 37 bitr4di ⊢ ( 𝜑 → ( ( 𝐹 ∘r 𝑅 𝐺 ∧ 𝐺 ∘r 𝑇 𝐻 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ∧ ( 𝐺 ‘ 𝑤 ) 𝑇 ( 𝐻 ‘ 𝑤 ) ) ) )
39 27 33 1 1 29 30 34 ofrfval ⊢ ( 𝜑 → ( 𝐹 ∘r 𝑈 𝐻 ↔ ∀ 𝑤 ∈ 𝐴 ( 𝐹 ‘ 𝑤 ) 𝑈 ( 𝐻 ‘ 𝑤 ) ) )
40 26 38 39 3imtr4d ⊢ ( 𝜑 → ( ( 𝐹 ∘r 𝑅 𝐺 ∧ 𝐺 ∘r 𝑇 𝐻 ) → 𝐹 ∘r 𝑈 𝐻 ) )