Metamath Proof Explorer


Theorem reprinrn

Description: Representations with term in an intersection. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses reprval.a φ A
reprval.m φ M
reprval.s φ S 0
Assertion reprinrn φ c A B repr S M c A repr S M ran c B

Proof

Step Hyp Ref Expression
1 reprval.a φ A
2 reprval.m φ M
3 reprval.s φ S 0
4 fin c : 0 ..^ S A B c : 0 ..^ S A c : 0 ..^ S B
5 df-f c : 0 ..^ S B c Fn 0 ..^ S ran c B
6 ffn c : 0 ..^ S A c Fn 0 ..^ S
7 6 adantl φ c : 0 ..^ S A c Fn 0 ..^ S
8 7 biantrurd φ c : 0 ..^ S A ran c B c Fn 0 ..^ S ran c B
9 8 bicomd φ c : 0 ..^ S A c Fn 0 ..^ S ran c B ran c B
10 5 9 syl5bb φ c : 0 ..^ S A c : 0 ..^ S B ran c B
11 10 pm5.32da φ c : 0 ..^ S A c : 0 ..^ S B c : 0 ..^ S A ran c B
12 4 11 syl5bb φ c : 0 ..^ S A B c : 0 ..^ S A ran c B
13 nnex V
14 13 a1i φ V
15 14 1 ssexd φ A V
16 inex1g A V A B V
17 15 16 syl φ A B V
18 ovex 0 ..^ S V
19 elmapg A B V 0 ..^ S V c A B 0 ..^ S c : 0 ..^ S A B
20 17 18 19 sylancl φ c A B 0 ..^ S c : 0 ..^ S A B
21 elmapg A V 0 ..^ S V c A 0 ..^ S c : 0 ..^ S A
22 15 18 21 sylancl φ c A 0 ..^ S c : 0 ..^ S A
23 22 anbi1d φ c A 0 ..^ S ran c B c : 0 ..^ S A ran c B
24 12 20 23 3bitr4d φ c A B 0 ..^ S c A 0 ..^ S ran c B
25 24 anbi1d φ c A B 0 ..^ S a 0 ..^ S c a = M c A 0 ..^ S ran c B a 0 ..^ S c a = M
26 inss1 A B A
27 26 1 sstrid φ A B
28 27 2 3 reprval φ A B repr S M = c A B 0 ..^ S | a 0 ..^ S c a = M
29 28 eleq2d φ c A B repr S M c c A B 0 ..^ S | a 0 ..^ S c a = M
30 rabid c c A B 0 ..^ S | a 0 ..^ S c a = M c A B 0 ..^ S a 0 ..^ S c a = M
31 29 30 bitrdi φ c A B repr S M c A B 0 ..^ S a 0 ..^ S c a = M
32 1 2 3 reprval φ A repr S M = c A 0 ..^ S | a 0 ..^ S c a = M
33 32 eleq2d φ c A repr S M c c A 0 ..^ S | a 0 ..^ S c a = M
34 rabid c c A 0 ..^ S | a 0 ..^ S c a = M c A 0 ..^ S a 0 ..^ S c a = M
35 33 34 bitrdi φ c A repr S M c A 0 ..^ S a 0 ..^ S c a = M
36 35 anbi1d φ c A repr S M ran c B c A 0 ..^ S a 0 ..^ S c a = M ran c B
37 an32 c A 0 ..^ S a 0 ..^ S c a = M ran c B c A 0 ..^ S ran c B a 0 ..^ S c a = M
38 36 37 bitrdi φ c A repr S M ran c B c A 0 ..^ S ran c B a 0 ..^ S c a = M
39 25 31 38 3bitr4d φ c A B repr S M c A repr S M ran c B