Metamath Proof Explorer

Theorem isthincd2lem1

Description: Lemma for isthincd2 and thincmo2 . (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd2lem1.1 ⊢ φ → X ∈ B
isthincd2lem1.2 ⊢ φ → Y ∈ B
isthincd2lem1.3 ⊢ φ → F ∈ X H Y
isthincd2lem1.4 ⊢ φ → G ∈ X H Y
isthincd2lem1.5 ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
Assertion isthincd2lem1 ⊢ φ → F = G

Proof

Step Hyp Ref Expression
1 isthincd2lem1.1 ⊢ φ → X ∈ B
2 isthincd2lem1.2 ⊢ φ → Y ∈ B
3 isthincd2lem1.3 ⊢ φ → F ∈ X H Y
4 isthincd2lem1.4 ⊢ φ → G ∈ X H Y
5 isthincd2lem1.5 ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
6 oveq1 ⊢ x = z → x H y = z H y
7 6 eleq2d ⊢ x = z → f ∈ x H y ↔ f ∈ z H y
8 7 mobidv ⊢ x = z → ∃* f f ∈ x H y ↔ ∃* f f ∈ z H y
9 oveq2 ⊢ y = w → z H y = z H w
10 9 eleq2d ⊢ y = w → f ∈ z H y ↔ f ∈ z H w
11 10 mobidv ⊢ y = w → ∃* f f ∈ z H y ↔ ∃* f f ∈ z H w
12 8 11 cbvral2vw ⊢ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y ↔ ∀ z ∈ B ∀ w ∈ B ∃* f f ∈ z H w
13 5 12 sylib ⊢ φ → ∀ z ∈ B ∀ w ∈ B ∃* f f ∈ z H w
14 oveq1 ⊢ z = X → z H w = X H w
15 14 eleq2d ⊢ z = X → f ∈ z H w ↔ f ∈ X H w
16 15 mobidv ⊢ z = X → ∃* f f ∈ z H w ↔ ∃* f f ∈ X H w
17 nfv ⊢ Ⅎ k f ∈ X H w
18 nfv ⊢ Ⅎ f k ∈ X H w
19 eleq1w ⊢ f = k → f ∈ X H w ↔ k ∈ X H w
20 17 18 19 cbvmow ⊢ ∃* f f ∈ X H w ↔ ∃* k k ∈ X H w
21 oveq2 ⊢ w = Y → X H w = X H Y
22 21 eleq2d ⊢ w = Y → k ∈ X H w ↔ k ∈ X H Y
23 22 mobidv ⊢ w = Y → ∃* k k ∈ X H w ↔ ∃* k k ∈ X H Y
24 20 23 bitrid ⊢ w = Y → ∃* f f ∈ X H w ↔ ∃* k k ∈ X H Y
25 eqidd ⊢ φ ∧ z = X → B = B
26 16 24 1 25 2 rspc2vd ⊢ φ → ∀ z ∈ B ∀ w ∈ B ∃* f f ∈ z H w → ∃* k k ∈ X H Y
27 13 26 mpd ⊢ φ → ∃* k k ∈ X H Y
28 moel ⊢ ∃* k k ∈ X H Y ↔ ∀ k ∈ X H Y ∀ l ∈ X H Y k = l
29 27 28 sylib ⊢ φ → ∀ k ∈ X H Y ∀ l ∈ X H Y k = l
30 eqeq1 ⊢ k = F → k = l ↔ F = l
31 eqeq2 ⊢ l = G → F = l ↔ F = G
32 eqidd ⊢ φ ∧ k = F → X H Y = X H Y
33 30 31 3 32 4 rspc2vd ⊢ φ → ∀ k ∈ X H Y ∀ l ∈ X H Y k = l → F = G
34 29 33 mpd ⊢ φ → F = G