Metamath Proof Explorer

Theorem relexp0eq

Description: The zeroth power of relationships is the same if and only if the union of their domain and ranges is the same. (Contributed by RP, 11-Jun-2020)

Ref Expression
Assertion relexp0eq ⊢A∈U∧B∈V→dom⁡A∪ran⁡A=dom⁡B∪ran⁡B↔A↑r0=B↑r0

Proof

Step Hyp Ref Expression
1 dfcleq ⊢dom⁡A∪ran⁡A=dom⁡B∪ran⁡B↔∀xx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B
2 alcom ⊢∀y∀xx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔∀x∀yx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B
3 19.3v ⊢∀y∀xx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔∀xx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B
4 ax6ev ⊢∃yy=x
5 pm5.5 ⊢∃yy=x→∃yy=x→x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B
6 4 5 ax-mp ⊢∃yy=x→x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B
7 19.23v ⊢∀yy=x→x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔∃yy=x→x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B
8 19.3v ⊢∀yx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B
9 6 7 8 3bitr4ri ⊢∀yx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔∀yy=x→x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B
10 pm5.32 ⊢y=x→x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔y=x∧x∈dom⁡A∪ran⁡A↔y=x∧x∈dom⁡B∪ran⁡B
11 ancom ⊢y=x∧x∈dom⁡A∪ran⁡A↔x∈dom⁡A∪ran⁡A∧y=x
12 ancom ⊢y=x∧x∈dom⁡B∪ran⁡B↔x∈dom⁡B∪ran⁡B∧y=x
13 11 12 bibi12i ⊢y=x∧x∈dom⁡A∪ran⁡A↔y=x∧x∈dom⁡B∪ran⁡B↔x∈dom⁡A∪ran⁡A∧y=x↔x∈dom⁡B∪ran⁡B∧y=x
14 10 13 bitri ⊢y=x→x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔x∈dom⁡A∪ran⁡A∧y=x↔x∈dom⁡B∪ran⁡B∧y=x
15 14 albii ⊢∀yy=x→x∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔∀yx∈dom⁡A∪ran⁡A∧y=x↔x∈dom⁡B∪ran⁡B∧y=x
16 9 15 bitri ⊢∀yx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔∀yx∈dom⁡A∪ran⁡A∧y=x↔x∈dom⁡B∪ran⁡B∧y=x
17 16 albii ⊢∀x∀yx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔∀x∀yx∈dom⁡A∪ran⁡A∧y=x↔x∈dom⁡B∪ran⁡B∧y=x
18 2 3 17 3bitr3i ⊢∀xx∈dom⁡A∪ran⁡A↔x∈dom⁡B∪ran⁡B↔∀x∀yx∈dom⁡A∪ran⁡A∧y=x↔x∈dom⁡B∪ran⁡B∧y=x
19 1 18 bitri ⊢dom⁡A∪ran⁡A=dom⁡B∪ran⁡B↔∀x∀yx∈dom⁡A∪ran⁡A∧y=x↔x∈dom⁡B∪ran⁡B∧y=x
20 eqopab2bw ⊢xy|x∈dom⁡A∪ran⁡A∧y=x=xy|x∈dom⁡B∪ran⁡B∧y=x↔∀x∀yx∈dom⁡A∪ran⁡A∧y=x↔x∈dom⁡B∪ran⁡B∧y=x
21 opabresid ⊢I↾dom⁡A∪ran⁡A=xy|x∈dom⁡A∪ran⁡A∧y=x
22 21 eqcomi ⊢xy|x∈dom⁡A∪ran⁡A∧y=x=I↾dom⁡A∪ran⁡A
23 opabresid ⊢I↾dom⁡B∪ran⁡B=xy|x∈dom⁡B∪ran⁡B∧y=x
24 23 eqcomi ⊢xy|x∈dom⁡B∪ran⁡B∧y=x=I↾dom⁡B∪ran⁡B
25 22 24 eqeq12i ⊢xy|x∈dom⁡A∪ran⁡A∧y=x=xy|x∈dom⁡B∪ran⁡B∧y=x↔I↾dom⁡A∪ran⁡A=I↾dom⁡B∪ran⁡B
26 19 20 25 3bitr2i ⊢dom⁡A∪ran⁡A=dom⁡B∪ran⁡B↔I↾dom⁡A∪ran⁡A=I↾dom⁡B∪ran⁡B
27 relexp0g ⊢A∈U→A↑r0=I↾dom⁡A∪ran⁡A
28 relexp0g ⊢B∈V→B↑r0=I↾dom⁡B∪ran⁡B
29 27 28 eqeqan12d ⊢A∈U∧B∈V→A↑r0=B↑r0↔I↾dom⁡A∪ran⁡A=I↾dom⁡B∪ran⁡B
30 26 29 bitr4id ⊢A∈U∧B∈V→dom⁡A∪ran⁡A=dom⁡B∪ran⁡B↔A↑r0=B↑r0