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 𝑈 𝐻 ) )