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 ( ( 𝐴𝑈𝐵𝑉 ) → ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ( 𝐴𝑟 0 ) = ( 𝐵𝑟 0 ) ) )

Proof

Step Hyp Ref Expression
1 dfcleq ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) )
2 alcom ( ∀ 𝑦𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑥𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) )
3 19.3v ( ∀ 𝑦𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) )
4 ax6ev 𝑦 𝑦 = 𝑥
5 pm5.5 ( ∃ 𝑦 𝑦 = 𝑥 → ( ( ∃ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) )
6 4 5 ax-mp ( ( ∃ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) )
7 19.23v ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( ∃ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) )
8 19.3v ( ∀ 𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) )
9 6 7 8 3bitr4ri ( ∀ 𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) )
10 pm5.32 ( ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( ( 𝑦 = 𝑥𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ) ↔ ( 𝑦 = 𝑥𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) )
11 ancom ( ( 𝑦 = 𝑥𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ) ↔ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) )
12 ancom ( ( 𝑦 = 𝑥𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) )
13 11 12 bibi12i ( ( ( 𝑦 = 𝑥𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ) ↔ ( 𝑦 = 𝑥𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
14 10 13 bitri ( ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
15 14 albii ( ∀ 𝑦 ( 𝑦 = 𝑥 → ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ) ↔ ∀ 𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
16 9 15 bitri ( ∀ 𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
17 16 albii ( ∀ 𝑥𝑦 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑥𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
18 2 3 17 3bitr3i ( ∀ 𝑥 ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ↔ 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ) ↔ ∀ 𝑥𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
19 1 18 bitri ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ∀ 𝑥𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
20 eqopab2bw ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) } ↔ ∀ 𝑥𝑦 ( ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) ↔ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
21 opabresid ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) }
22 21 eqcomi { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) } = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) )
23 opabresid ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) }
24 23 eqcomi { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) } = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) )
25 22 24 eqeq12i ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( dom 𝐴 ∪ ran 𝐴 ) ∧ 𝑦 = 𝑥 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( dom 𝐵 ∪ ran 𝐵 ) ∧ 𝑦 = 𝑥 ) } ↔ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) )
26 19 20 25 3bitr2i ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) )
27 relexp0g ( 𝐴𝑈 → ( 𝐴𝑟 0 ) = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
28 relexp0g ( 𝐵𝑉 → ( 𝐵𝑟 0 ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) )
29 27 28 eqeqan12d ( ( 𝐴𝑈𝐵𝑉 ) → ( ( 𝐴𝑟 0 ) = ( 𝐵𝑟 0 ) ↔ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( I ↾ ( dom 𝐵 ∪ ran 𝐵 ) ) ) )
30 26 29 bitr4id ( ( 𝐴𝑈𝐵𝑉 ) → ( ( dom 𝐴 ∪ ran 𝐴 ) = ( dom 𝐵 ∪ ran 𝐵 ) ↔ ( 𝐴𝑟 0 ) = ( 𝐵𝑟 0 ) ) )