Metamath Proof Explorer

Theorem ssrelf

Description: A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of Monk1 p. 33. (Contributed by NM, 2-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Revised by Thierry Arnoux, 6-Nov-2017)

Ref Expression
Hypotheses eqrelrd2.1 ⊢Ⅎxφ
eqrelrd2.2 ⊢Ⅎyφ
eqrelrd2.3 ⊢Ⅎ_xA
eqrelrd2.4 ⊢Ⅎ_yA
eqrelrd2.5 ⊢Ⅎ_xB
eqrelrd2.6 ⊢Ⅎ_yB
Assertion ssrelf ⊢Rel⁡A→A⊆B↔∀x∀yxy∈A→xy∈B

Proof

Step Hyp Ref Expression
1 eqrelrd2.1 ⊢Ⅎxφ
2 eqrelrd2.2 ⊢Ⅎyφ
3 eqrelrd2.3 ⊢Ⅎ_xA
4 eqrelrd2.4 ⊢Ⅎ_yA
5 eqrelrd2.5 ⊢Ⅎ_xB
6 eqrelrd2.6 ⊢Ⅎ_yB
7 3 5 nfss ⊢ℲxA⊆B
8 4 6 nfss ⊢ℲyA⊆B
9 ssel ⊢A⊆B→xy∈A→xy∈B
10 8 9 alrimi ⊢A⊆B→∀yxy∈A→xy∈B
11 7 10 alrimi ⊢A⊆B→∀x∀yxy∈A→xy∈B
12 eleq1 ⊢z=xy→z∈A↔xy∈A
13 eleq1 ⊢z=xy→z∈B↔xy∈B
14 12 13 imbi12d ⊢z=xy→z∈A→z∈B↔xy∈A→xy∈B
15 14 biimprcd ⊢xy∈A→xy∈B→z=xy→z∈A→z∈B
16 15 2alimi ⊢∀x∀yxy∈A→xy∈B→∀x∀yz=xy→z∈A→z∈B
17 4 nfcri ⊢Ⅎyz∈A
18 6 nfcri ⊢Ⅎyz∈B
19 17 18 nfim ⊢Ⅎyz∈A→z∈B
20 19 19.23 ⊢∀yz=xy→z∈A→z∈B↔∃yz=xy→z∈A→z∈B
21 20 albii ⊢∀x∀yz=xy→z∈A→z∈B↔∀x∃yz=xy→z∈A→z∈B
22 3 nfcri ⊢Ⅎxz∈A
23 5 nfcri ⊢Ⅎxz∈B
24 22 23 nfim ⊢Ⅎxz∈A→z∈B
25 24 19.23 ⊢∀x∃yz=xy→z∈A→z∈B↔∃x∃yz=xy→z∈A→z∈B
26 21 25 bitri ⊢∀x∀yz=xy→z∈A→z∈B↔∃x∃yz=xy→z∈A→z∈B
27 16 26 sylib ⊢∀x∀yxy∈A→xy∈B→∃x∃yz=xy→z∈A→z∈B
28 27 com23 ⊢∀x∀yxy∈A→xy∈B→z∈A→∃x∃yz=xy→z∈B
29 28 a2d ⊢∀x∀yxy∈A→xy∈B→z∈A→∃x∃yz=xy→z∈A→z∈B
30 29 alimdv ⊢∀x∀yxy∈A→xy∈B→∀zz∈A→∃x∃yz=xy→∀zz∈A→z∈B
31 df-rel ⊢Rel⁡A↔A⊆V×V
32 dfss2 ⊢A⊆V×V↔∀zz∈A→z∈V×V
33 elvv ⊢z∈V×V↔∃x∃yz=xy
34 33 imbi2i ⊢z∈A→z∈V×V↔z∈A→∃x∃yz=xy
35 34 albii ⊢∀zz∈A→z∈V×V↔∀zz∈A→∃x∃yz=xy
36 31 32 35 3bitri ⊢Rel⁡A↔∀zz∈A→∃x∃yz=xy
37 dfss2 ⊢A⊆B↔∀zz∈A→z∈B
38 30 36 37 3imtr4g ⊢∀x∀yxy∈A→xy∈B→Rel⁡A→A⊆B
39 38 com12 ⊢Rel⁡A→∀x∀yxy∈A→xy∈B→A⊆B
40 11 39 impbid2 ⊢Rel⁡A→A⊆B↔∀x∀yxy∈A→xy∈B