Metamath Proof Explorer

Theorem bnj554

Description: Technical lemma for bnj852 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj554.19 ⊢ η ↔ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ ω ∧ m = suc ⁡ p
bnj554.20 ⊢ ζ ↔ i ∈ ω ∧ suc ⁡ i ∈ n ∧ m = suc ⁡ i
bnj554.21 ⊢ K = ⋃ y ∈ G ⁡ i pred y A R
bnj554.22 ⊢ L = ⋃ y ∈ G ⁡ p pred y A R
bnj554.23 ⊢ K = ⋃ y ∈ G ⁡ i pred y A R
bnj554.24 ⊢ L = ⋃ y ∈ G ⁡ p pred y A R
Assertion bnj554 ⊢ η ∧ ζ → G ⁡ m = L ↔ G ⁡ suc ⁡ i = K

Proof

Step Hyp Ref Expression
1 bnj554.19 ⊢ η ↔ m ∈ D ∧ n = suc ⁡ m ∧ p ∈ ω ∧ m = suc ⁡ p
2 bnj554.20 ⊢ ζ ↔ i ∈ ω ∧ suc ⁡ i ∈ n ∧ m = suc ⁡ i
3 bnj554.21 ⊢ K = ⋃ y ∈ G ⁡ i pred y A R
4 bnj554.22 ⊢ L = ⋃ y ∈ G ⁡ p pred y A R
5 bnj554.23 ⊢ K = ⋃ y ∈ G ⁡ i pred y A R
6 bnj554.24 ⊢ L = ⋃ y ∈ G ⁡ p pred y A R
7 1 bnj1254 ⊢ η → m = suc ⁡ p
8 2 simp3bi ⊢ ζ → m = suc ⁡ i
9 simpr ⊢ m = suc ⁡ p ∧ m = suc ⁡ i → m = suc ⁡ i
10 bnj551 ⊢ m = suc ⁡ p ∧ m = suc ⁡ i → p = i
11 fveq2 ⊢ m = suc ⁡ i → G ⁡ m = G ⁡ suc ⁡ i
12 fveq2 ⊢ p = i → G ⁡ p = G ⁡ i
13 iuneq1 ⊢ G ⁡ p = G ⁡ i → ⋃ y ∈ G ⁡ p pred y A R = ⋃ y ∈ G ⁡ i pred y A R
14 13 6 5 3eqtr4g ⊢ G ⁡ p = G ⁡ i → L = K
15 12 14 syl ⊢ p = i → L = K
16 11 15 eqeqan12d ⊢ m = suc ⁡ i ∧ p = i → G ⁡ m = L ↔ G ⁡ suc ⁡ i = K
17 9 10 16 syl2anc ⊢ m = suc ⁡ p ∧ m = suc ⁡ i → G ⁡ m = L ↔ G ⁡ suc ⁡ i = K
18 7 8 17 syl2an ⊢ η ∧ ζ → G ⁡ m = L ↔ G ⁡ suc ⁡ i = K