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∈XHY
isthincd2lem1.4 ⊢φ→G∈XHY
isthincd2lem1.5 ⊢φ→∀x∈B∀y∈B∃*ff∈xHy
Assertion isthincd2lem1 ⊢φ→F=G

Proof

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