Metamath Proof Explorer

Theorem undmrnresiss

Description: Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg . (Contributed by RP, 26-Sep-2020)

Ref Expression
Assertion undmrnresiss ⊢I↾dom⁡A∪ran⁡A⊆B↔∀x∀yxAy→xBx∧yBy

Proof

Step Hyp Ref Expression
1 resundi ⊢I↾dom⁡A∪ran⁡A=I↾dom⁡A∪I↾ran⁡A
2 1 sseq1i ⊢I↾dom⁡A∪ran⁡A⊆B↔I↾dom⁡A∪I↾ran⁡A⊆B
3 unss ⊢I↾dom⁡A⊆B∧I↾ran⁡A⊆B↔I↾dom⁡A∪I↾ran⁡A⊆B
4 relres ⊢Rel⁡I↾dom⁡A
5 ssrel ⊢Rel⁡I↾dom⁡A→I↾dom⁡A⊆B↔∀x∀zxz∈I↾dom⁡A→xz∈B
6 4 5 ax-mp ⊢I↾dom⁡A⊆B↔∀x∀zxz∈I↾dom⁡A→xz∈B
7 vex ⊢x∈V
8 7 eldm ⊢x∈dom⁡A↔∃yxAy
9 df-br ⊢xIz↔xz∈I
10 vex ⊢z∈V
11 10 ideq ⊢xIz↔x=z
12 9 11 bitr3i ⊢xz∈I↔x=z
13 8 12 anbi12ci ⊢x∈dom⁡A∧xz∈I↔x=z∧∃yxAy
14 10 opelresi ⊢xz∈I↾dom⁡A↔x∈dom⁡A∧xz∈I
15 19.42v ⊢∃yx=z∧xAy↔x=z∧∃yxAy
16 13 14 15 3bitr4i ⊢xz∈I↾dom⁡A↔∃yx=z∧xAy
17 df-br ⊢xBz↔xz∈B
18 17 bicomi ⊢xz∈B↔xBz
19 16 18 imbi12i ⊢xz∈I↾dom⁡A→xz∈B↔∃yx=z∧xAy→xBz
20 19 2albii ⊢∀x∀zxz∈I↾dom⁡A→xz∈B↔∀x∀z∃yx=z∧xAy→xBz
21 19.23v ⊢∀yx=z∧xAy→xBz↔∃yx=z∧xAy→xBz
22 21 bicomi ⊢∃yx=z∧xAy→xBz↔∀yx=z∧xAy→xBz
23 22 2albii ⊢∀x∀z∃yx=z∧xAy→xBz↔∀x∀z∀yx=z∧xAy→xBz
24 alcom ⊢∀z∀yx=z∧xAy→xBz↔∀y∀zx=z∧xAy→xBz
25 ancomst ⊢x=z∧xAy→xBz↔xAy∧x=z→xBz
26 impexp ⊢xAy∧x=z→xBz↔xAy→x=z→xBz
27 25 26 bitri ⊢x=z∧xAy→xBz↔xAy→x=z→xBz
28 27 albii ⊢∀zx=z∧xAy→xBz↔∀zxAy→x=z→xBz
29 19.21v ⊢∀zxAy→x=z→xBz↔xAy→∀zx=z→xBz
30 equcom ⊢x=z↔z=x
31 30 imbi1i ⊢x=z→xBz↔z=x→xBz
32 31 albii ⊢∀zx=z→xBz↔∀zz=x→xBz
33 breq2 ⊢z=x→xBz↔xBx
34 33 equsalvw ⊢∀zz=x→xBz↔xBx
35 32 34 bitri ⊢∀zx=z→xBz↔xBx
36 35 imbi2i ⊢xAy→∀zx=z→xBz↔xAy→xBx
37 28 29 36 3bitri ⊢∀zx=z∧xAy→xBz↔xAy→xBx
38 37 albii ⊢∀y∀zx=z∧xAy→xBz↔∀yxAy→xBx
39 24 38 bitri ⊢∀z∀yx=z∧xAy→xBz↔∀yxAy→xBx
40 39 albii ⊢∀x∀z∀yx=z∧xAy→xBz↔∀x∀yxAy→xBx
41 23 40 bitri ⊢∀x∀z∃yx=z∧xAy→xBz↔∀x∀yxAy→xBx
42 6 20 41 3bitri ⊢I↾dom⁡A⊆B↔∀x∀yxAy→xBx
43 relres ⊢Rel⁡I↾ran⁡A
44 ssrel ⊢Rel⁡I↾ran⁡A→I↾ran⁡A⊆B↔∀y∀zyz∈I↾ran⁡A→yz∈B
45 43 44 ax-mp ⊢I↾ran⁡A⊆B↔∀y∀zyz∈I↾ran⁡A→yz∈B
46 vex ⊢y∈V
47 46 elrn ⊢y∈ran⁡A↔∃xxAy
48 df-br ⊢yIz↔yz∈I
49 10 ideq ⊢yIz↔y=z
50 48 49 bitr3i ⊢yz∈I↔y=z
51 47 50 anbi12ci ⊢y∈ran⁡A∧yz∈I↔y=z∧∃xxAy
52 10 opelresi ⊢yz∈I↾ran⁡A↔y∈ran⁡A∧yz∈I
53 19.42v ⊢∃xy=z∧xAy↔y=z∧∃xxAy
54 51 52 53 3bitr4i ⊢yz∈I↾ran⁡A↔∃xy=z∧xAy
55 df-br ⊢yBz↔yz∈B
56 55 bicomi ⊢yz∈B↔yBz
57 54 56 imbi12i ⊢yz∈I↾ran⁡A→yz∈B↔∃xy=z∧xAy→yBz
58 57 2albii ⊢∀y∀zyz∈I↾ran⁡A→yz∈B↔∀y∀z∃xy=z∧xAy→yBz
59 19.23v ⊢∀xy=z∧xAy→yBz↔∃xy=z∧xAy→yBz
60 59 bicomi ⊢∃xy=z∧xAy→yBz↔∀xy=z∧xAy→yBz
61 60 2albii ⊢∀y∀z∃xy=z∧xAy→yBz↔∀y∀z∀xy=z∧xAy→yBz
62 alrot3 ⊢∀x∀y∀zy=z∧xAy→yBz↔∀y∀z∀xy=z∧xAy→yBz
63 ancomst ⊢y=z∧xAy→yBz↔xAy∧y=z→yBz
64 impexp ⊢xAy∧y=z→yBz↔xAy→y=z→yBz
65 63 64 bitri ⊢y=z∧xAy→yBz↔xAy→y=z→yBz
66 65 albii ⊢∀zy=z∧xAy→yBz↔∀zxAy→y=z→yBz
67 19.21v ⊢∀zxAy→y=z→yBz↔xAy→∀zy=z→yBz
68 equcom ⊢y=z↔z=y
69 68 imbi1i ⊢y=z→yBz↔z=y→yBz
70 69 albii ⊢∀zy=z→yBz↔∀zz=y→yBz
71 breq2 ⊢z=y→yBz↔yBy
72 71 equsalvw ⊢∀zz=y→yBz↔yBy
73 70 72 bitri ⊢∀zy=z→yBz↔yBy
74 73 imbi2i ⊢xAy→∀zy=z→yBz↔xAy→yBy
75 66 67 74 3bitri ⊢∀zy=z∧xAy→yBz↔xAy→yBy
76 75 2albii ⊢∀x∀y∀zy=z∧xAy→yBz↔∀x∀yxAy→yBy
77 61 62 76 3bitr2i ⊢∀y∀z∃xy=z∧xAy→yBz↔∀x∀yxAy→yBy
78 45 58 77 3bitri ⊢I↾ran⁡A⊆B↔∀x∀yxAy→yBy
79 42 78 anbi12i ⊢I↾dom⁡A⊆B∧I↾ran⁡A⊆B↔∀x∀yxAy→xBx∧∀x∀yxAy→yBy
80 19.26-2 ⊢∀x∀yxAy→xBx∧xAy→yBy↔∀x∀yxAy→xBx∧∀x∀yxAy→yBy
81 pm4.76 ⊢xAy→xBx∧xAy→yBy↔xAy→xBx∧yBy
82 81 2albii ⊢∀x∀yxAy→xBx∧xAy→yBy↔∀x∀yxAy→xBx∧yBy
83 79 80 82 3bitr2i ⊢I↾dom⁡A⊆B∧I↾ran⁡A⊆B↔∀x∀yxAy→xBx∧yBy
84 2 3 83 3bitr2i ⊢I↾dom⁡A∪ran⁡A⊆B↔∀x∀yxAy→xBx∧yBy