Metamath Proof Explorer


Theorem mapss2

Description: Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses mapss2.a ( 𝜑𝐴𝑉 )
mapss2.b ( 𝜑𝐵𝑊 )
mapss2.c ( 𝜑𝐶𝑍 )
mapss2.n ( 𝜑𝐶 ≠ ∅ )
Assertion mapss2 ( 𝜑 → ( 𝐴𝐵 ↔ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 mapss2.a ( 𝜑𝐴𝑉 )
2 mapss2.b ( 𝜑𝐵𝑊 )
3 mapss2.c ( 𝜑𝐶𝑍 )
4 mapss2.n ( 𝜑𝐶 ≠ ∅ )
5 2 adantr ( ( 𝜑𝐴𝐵 ) → 𝐵𝑊 )
6 simpr ( ( 𝜑𝐴𝐵 ) → 𝐴𝐵 )
7 mapss ( ( 𝐵𝑊𝐴𝐵 ) → ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) )
8 5 6 7 syl2anc ( ( 𝜑𝐴𝐵 ) → ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) )
9 8 ex ( 𝜑 → ( 𝐴𝐵 → ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) )
10 n0 ( 𝐶 ≠ ∅ ↔ ∃ 𝑥 𝑥𝐶 )
11 4 10 sylib ( 𝜑 → ∃ 𝑥 𝑥𝐶 )
12 11 adantr ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) → ∃ 𝑥 𝑥𝐶 )
13 eqidd ( ( 𝜑𝑥𝐶 ) → ( 𝑤𝐶𝑦 ) = ( 𝑤𝐶𝑦 ) )
14 eqidd ( ( ( 𝜑𝑥𝐶 ) ∧ 𝑤 = 𝑥 ) → 𝑦 = 𝑦 )
15 simpr ( ( 𝜑𝑥𝐶 ) → 𝑥𝐶 )
16 vex 𝑦 ∈ V
17 16 a1i ( ( 𝜑𝑥𝐶 ) → 𝑦 ∈ V )
18 13 14 15 17 fvmptd ( ( 𝜑𝑥𝐶 ) → ( ( 𝑤𝐶𝑦 ) ‘ 𝑥 ) = 𝑦 )
19 18 eqcomd ( ( 𝜑𝑥𝐶 ) → 𝑦 = ( ( 𝑤𝐶𝑦 ) ‘ 𝑥 ) )
20 19 ad4ant13 ( ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑥𝐶 ) ∧ 𝑦𝐴 ) → 𝑦 = ( ( 𝑤𝐶𝑦 ) ‘ 𝑥 ) )
21 simplr ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑦𝐴 ) → ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) )
22 simplr ( ( ( 𝜑𝑦𝐴 ) ∧ 𝑤𝐶 ) → 𝑦𝐴 )
23 22 fmpttd ( ( 𝜑𝑦𝐴 ) → ( 𝑤𝐶𝑦 ) : 𝐶𝐴 )
24 1 adantr ( ( 𝜑𝑦𝐴 ) → 𝐴𝑉 )
25 3 adantr ( ( 𝜑𝑦𝐴 ) → 𝐶𝑍 )
26 24 25 elmapd ( ( 𝜑𝑦𝐴 ) → ( ( 𝑤𝐶𝑦 ) ∈ ( 𝐴m 𝐶 ) ↔ ( 𝑤𝐶𝑦 ) : 𝐶𝐴 ) )
27 23 26 mpbird ( ( 𝜑𝑦𝐴 ) → ( 𝑤𝐶𝑦 ) ∈ ( 𝐴m 𝐶 ) )
28 27 adantlr ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑦𝐴 ) → ( 𝑤𝐶𝑦 ) ∈ ( 𝐴m 𝐶 ) )
29 21 28 sseldd ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑦𝐴 ) → ( 𝑤𝐶𝑦 ) ∈ ( 𝐵m 𝐶 ) )
30 elmapi ( ( 𝑤𝐶𝑦 ) ∈ ( 𝐵m 𝐶 ) → ( 𝑤𝐶𝑦 ) : 𝐶𝐵 )
31 29 30 syl ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑦𝐴 ) → ( 𝑤𝐶𝑦 ) : 𝐶𝐵 )
32 31 adantlr ( ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑥𝐶 ) ∧ 𝑦𝐴 ) → ( 𝑤𝐶𝑦 ) : 𝐶𝐵 )
33 simplr ( ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑥𝐶 ) ∧ 𝑦𝐴 ) → 𝑥𝐶 )
34 32 33 ffvelrnd ( ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑥𝐶 ) ∧ 𝑦𝐴 ) → ( ( 𝑤𝐶𝑦 ) ‘ 𝑥 ) ∈ 𝐵 )
35 20 34 eqeltrd ( ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑥𝐶 ) ∧ 𝑦𝐴 ) → 𝑦𝐵 )
36 35 ralrimiva ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑥𝐶 ) → ∀ 𝑦𝐴 𝑦𝐵 )
37 dfss3 ( 𝐴𝐵 ↔ ∀ 𝑦𝐴 𝑦𝐵 )
38 36 37 sylibr ( ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) ∧ 𝑥𝐶 ) → 𝐴𝐵 )
39 38 ex ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) → ( 𝑥𝐶𝐴𝐵 ) )
40 39 exlimdv ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) → ( ∃ 𝑥 𝑥𝐶𝐴𝐵 ) )
41 12 40 mpd ( ( 𝜑 ∧ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) → 𝐴𝐵 )
42 41 ex ( 𝜑 → ( ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) → 𝐴𝐵 ) )
43 9 42 impbid ( 𝜑 → ( 𝐴𝐵 ↔ ( 𝐴m 𝐶 ) ⊆ ( 𝐵m 𝐶 ) ) )