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 ↑ r 0 = B ↑ r 0

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ dom ⁡ A ∪ ran ⁡ A = dom ⁡ B ∪ ran ⁡ B ↔ ∀ x x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B
2 alcom ⊢ ∀ y ∀ x x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ ∀ x ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B
3 19.3v ⊢ ∀ y ∀ x x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ ∀ x x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B
4 ax6ev ⊢ ∃ y y = x
5 pm5.5 ⊢ ∃ y y = x → ∃ y y = 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 ⊢ ∃ y y = x → x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B
7 19.23v ⊢ ∀ y y = x → x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ ∃ y y = x → x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B
8 19.3v ⊢ ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B
9 6 7 8 3bitr4ri ⊢ ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ ∀ y y = 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 ⊢ ∀ y y = x → x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ∧ y = x
16 9 15 bitri ⊢ ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ∧ y = x
17 16 albii ⊢ ∀ x ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ ∀ x ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ∧ y = x
18 2 3 17 3bitr3i ⊢ ∀ x x ∈ dom ⁡ A ∪ ran ⁡ A ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ↔ ∀ x ∀ y x ∈ 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 ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ∧ y = x
20 eqopab2bw ⊢ x y | x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x = x y | x ∈ dom ⁡ B ∪ ran ⁡ B ∧ y = x ↔ ∀ x ∀ y x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x ↔ x ∈ dom ⁡ B ∪ ran ⁡ B ∧ y = x
21 opabresid ⊢ I ↾ dom ⁡ A ∪ ran ⁡ A = x y | x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x
22 21 eqcomi ⊢ x y | x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x = I ↾ dom ⁡ A ∪ ran ⁡ A
23 opabresid ⊢ I ↾ dom ⁡ B ∪ ran ⁡ B = x y | x ∈ dom ⁡ B ∪ ran ⁡ B ∧ y = x
24 23 eqcomi ⊢ x y | x ∈ dom ⁡ B ∪ ran ⁡ B ∧ y = x = I ↾ dom ⁡ B ∪ ran ⁡ B
25 22 24 eqeq12i ⊢ x y | x ∈ dom ⁡ A ∪ ran ⁡ A ∧ y = x = x y | 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 ↑ r 0 = I ↾ dom ⁡ A ∪ ran ⁡ A
28 relexp0g ⊢ B ∈ V → B ↑ r 0 = I ↾ dom ⁡ B ∪ ran ⁡ B
29 27 28 eqeqan12d ⊢ A ∈ U ∧ B ∈ V → A ↑ r 0 = B ↑ r 0 ↔ 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 ↑ r 0 = B ↑ r 0