Metamath Proof Explorer


Theorem isf33lem

Description: Lemma for isfin3-3 . (Contributed by Stefan O'Rear, 17-May-2015)

Ref Expression
Assertion isf33lem FinIII = g | a 𝒫 g ω x ω a suc x a x ran a ran a

Proof

Step Hyp Ref Expression
1 isfin32i f FinIII ¬ ω * f
2 fveq1 a = b a suc x = b suc x
3 fveq1 a = b a x = b x
4 2 3 sseq12d a = b a suc x a x b suc x b x
5 4 ralbidv a = b x ω a suc x a x x ω b suc x b x
6 rneq a = b ran a = ran b
7 6 inteqd a = b ran a = ran b
8 7 6 eleq12d a = b ran a ran a ran b ran b
9 5 8 imbi12d a = b x ω a suc x a x ran a ran a x ω b suc x b x ran b ran b
10 9 cbvralvw a 𝒫 g ω x ω a suc x a x ran a ran a b 𝒫 g ω x ω b suc x b x ran b ran b
11 pweq g = y 𝒫 g = 𝒫 y
12 11 oveq1d g = y 𝒫 g ω = 𝒫 y ω
13 12 raleqdv g = y b 𝒫 g ω x ω b suc x b x ran b ran b b 𝒫 y ω x ω b suc x b x ran b ran b
14 10 13 syl5bb g = y a 𝒫 g ω x ω a suc x a x ran a ran a b 𝒫 y ω x ω b suc x b x ran b ran b
15 14 cbvabv g | a 𝒫 g ω x ω a suc x a x ran a ran a = y | b 𝒫 y ω x ω b suc x b x ran b ran b
16 15 isf32lem12 f FinIII ¬ ω * f f g | a 𝒫 g ω x ω a suc x a x ran a ran a
17 1 16 mpd f FinIII f g | a 𝒫 g ω x ω a suc x a x ran a ran a
18 10 abbii g | a 𝒫 g ω x ω a suc x a x ran a ran a = g | b 𝒫 g ω x ω b suc x b x ran b ran b
19 18 fin23lem41 f g | a 𝒫 g ω x ω a suc x a x ran a ran a f FinIII
20 17 19 impbii f FinIII f g | a 𝒫 g ω x ω a suc x a x ran a ran a
21 20 eqriv FinIII = g | a 𝒫 g ω x ω a suc x a x ran a ran a