Metamath Proof Explorer

Theorem wsuclb

Description: A well-founded successor is a lower bound on points after X . (Contributed by Scott Fenton, 16-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

Ref Expression
Hypotheses wsuclb.1 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
wsuclb.2 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
wsuclb.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
wsuclb.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
wsuclb.5 ⊢ ( 𝜑 → 𝑋 𝑅 𝑌 )
Assertion wsuclb ( 𝜑 → ¬ 𝑌 𝑅 wsuc ( 𝑅 , 𝐴 , 𝑋 ) )

Proof

Step Hyp Ref Expression
1 wsuclb.1 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
2 wsuclb.2 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
3 wsuclb.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4 wsuclb.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
5 wsuclb.5 ⊢ ( 𝜑 → 𝑋 𝑅 𝑌 )
6 brcnvg ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑌 ◡ 𝑅 𝑋 ↔ 𝑋 𝑅 𝑌 ) )
7 4 3 6 syl2anc ⊢ ( 𝜑 → ( 𝑌 ◡ 𝑅 𝑋 ↔ 𝑋 𝑅 𝑌 ) )
8 5 7 mpbird ⊢ ( 𝜑 → 𝑌 ◡ 𝑅 𝑋 )
9 elpredg ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 ◡ 𝑅 𝑋 ) )
10 3 4 9 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 ◡ 𝑅 𝑋 ) )
11 8 10 mpbird ⊢ ( 𝜑 → 𝑌 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) )
12 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
13 1 12 syl ⊢ ( 𝜑 → 𝑅 Or 𝐴 )
14 breq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝑅 𝑦 ↔ 𝑋 𝑅 𝑌 ) )
15 14 rspcev ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑋 𝑅 𝑌 ) → ∃ 𝑦 ∈ 𝐴 𝑋 𝑅 𝑦 )
16 4 5 15 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 𝑋 𝑅 𝑦 )
17 1 2 3 16 wsuclem ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐴 ( ∀ 𝑏 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑏 𝑅 𝑎 ∧ ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 → ∃ 𝑐 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑐 𝑅 𝑏 ) ) )
18 13 17 inflb ⊢ ( 𝜑 → ( 𝑌 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) → ¬ 𝑌 𝑅 inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ) )
19 11 18 mpd ⊢ ( 𝜑 → ¬ 𝑌 𝑅 inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) )
20 df-wsuc ⊢ wsuc ( 𝑅 , 𝐴 , 𝑋 ) = inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 )
21 20 breq2i ⊢ ( 𝑌 𝑅 wsuc ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) )
22 19 21 sylnibr ⊢ ( 𝜑 → ¬ 𝑌 𝑅 wsuc ( 𝑅 , 𝐴 , 𝑋 ) )