Metamath Proof Explorer


Theorem omsindsOLD

Description: Obsolete version of omsinds as of 16-Oct-2024. (Contributed by Scott Fenton, 17-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses omsinds.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
omsinds.2 ( 𝑥 = 𝐴 → ( 𝜑𝜒 ) )
omsinds.3 ( 𝑥 ∈ ω → ( ∀ 𝑦𝑥 𝜓𝜑 ) )
Assertion omsindsOLD ( 𝐴 ∈ ω → 𝜒 )

Proof

Step Hyp Ref Expression
1 omsinds.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 omsinds.2 ( 𝑥 = 𝐴 → ( 𝜑𝜒 ) )
3 omsinds.3 ( 𝑥 ∈ ω → ( ∀ 𝑦𝑥 𝜓𝜑 ) )
4 omsson ω ⊆ On
5 epweon E We On
6 wess ( ω ⊆ On → ( E We On → E We ω ) )
7 4 5 6 mp2 E We ω
8 epse E Se ω
9 predep ( 𝑥 ∈ ω → Pred ( E , ω , 𝑥 ) = ( ω ∩ 𝑥 ) )
10 ordom Ord ω
11 ordtr ( Ord ω → Tr ω )
12 trss ( Tr ω → ( 𝑥 ∈ ω → 𝑥 ⊆ ω ) )
13 10 11 12 mp2b ( 𝑥 ∈ ω → 𝑥 ⊆ ω )
14 sseqin2 ( 𝑥 ⊆ ω ↔ ( ω ∩ 𝑥 ) = 𝑥 )
15 13 14 sylib ( 𝑥 ∈ ω → ( ω ∩ 𝑥 ) = 𝑥 )
16 9 15 eqtrd ( 𝑥 ∈ ω → Pred ( E , ω , 𝑥 ) = 𝑥 )
17 16 raleqdv ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ Pred ( E , ω , 𝑥 ) 𝜓 ↔ ∀ 𝑦𝑥 𝜓 ) )
18 17 3 sylbid ( 𝑥 ∈ ω → ( ∀ 𝑦 ∈ Pred ( E , ω , 𝑥 ) 𝜓𝜑 ) )
19 7 8 1 2 18 wfis3 ( 𝐴 ∈ ω → 𝜒 )