Metamath Proof Explorer

Theorem wsuclem

Description: Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018) (Revised by AV, 10-Oct-2021)

Ref Expression
Hypotheses wsuclem.1 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
wsuclem.2 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
wsuclem.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
wsuclem.4 ⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝐴 𝑋 𝑅 𝑤 )
Assertion wsuclem ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 wsuclem.1 ⊢ ( 𝜑 → 𝑅 We 𝐴 )
2 wsuclem.2 ⊢ ( 𝜑 → 𝑅 Se 𝐴 )
3 wsuclem.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4 wsuclem.4 ⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝐴 𝑋 𝑅 𝑤 )
5 predss ⊢ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴
6 5 a1i ⊢ ( 𝜑 → Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴 )
7 dfpred3g ⊢ ( 𝑋 ∈ 𝑉 → Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) = { 𝑤 ∈ 𝐴 ∣ 𝑤 ◡ 𝑅 𝑋 } )
8 3 7 syl ⊢ ( 𝜑 → Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) = { 𝑤 ∈ 𝐴 ∣ 𝑤 ◡ 𝑅 𝑋 } )
9 3 elexd ⊢ ( 𝜑 → 𝑋 ∈ V )
10 rabn0 ⊢ ( { 𝑤 ∈ 𝐴 ∣ 𝑤 ◡ 𝑅 𝑋 } ≠ ∅ ↔ ∃ 𝑤 ∈ 𝐴 𝑤 ◡ 𝑅 𝑋 )
11 brcnvg ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑋 ∈ V ) → ( 𝑤 ◡ 𝑅 𝑋 ↔ 𝑋 𝑅 𝑤 ) )
12 11 ancoms ⊢ ( ( 𝑋 ∈ V ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 ◡ 𝑅 𝑋 ↔ 𝑋 𝑅 𝑤 ) )
13 12 rexbidva ⊢ ( 𝑋 ∈ V → ( ∃ 𝑤 ∈ 𝐴 𝑤 ◡ 𝑅 𝑋 ↔ ∃ 𝑤 ∈ 𝐴 𝑋 𝑅 𝑤 ) )
14 10 13 syl5bb ⊢ ( 𝑋 ∈ V → ( { 𝑤 ∈ 𝐴 ∣ 𝑤 ◡ 𝑅 𝑋 } ≠ ∅ ↔ ∃ 𝑤 ∈ 𝐴 𝑋 𝑅 𝑤 ) )
15 14 biimpar ⊢ ( ( 𝑋 ∈ V ∧ ∃ 𝑤 ∈ 𝐴 𝑋 𝑅 𝑤 ) → { 𝑤 ∈ 𝐴 ∣ 𝑤 ◡ 𝑅 𝑋 } ≠ ∅ )
16 9 4 15 syl2anc ⊢ ( 𝜑 → { 𝑤 ∈ 𝐴 ∣ 𝑤 ◡ 𝑅 𝑋 } ≠ ∅ )
17 8 16 eqnetrd ⊢ ( 𝜑 → Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ≠ ∅ )
18 tz6.26 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴 ∧ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ≠ ∅ ) ) → ∃ 𝑥 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ )
19 1 2 6 17 18 syl22anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ )
20 dfpred3g ⊢ ( 𝑋 ∈ 𝑉 → Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 ◡ 𝑅 𝑋 } )
21 3 20 syl ⊢ ( 𝜑 → Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 ◡ 𝑅 𝑋 } )
22 21 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ↔ ∃ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ◡ 𝑅 𝑋 } Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) )
23 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ◡ 𝑅 𝑋 ↔ 𝑥 ◡ 𝑅 𝑋 ) )
24 23 rexrab ⊢ ( ∃ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ◡ 𝑅 𝑋 } Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑥 ◡ 𝑅 𝑋 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) )
25 noel ⊢ ¬ 𝑦 ∈ ∅
26 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ )
27 26 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → ( 𝑦 ∈ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) ↔ 𝑦 ∈ ∅ ) )
28 25 27 mtbiri ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → ¬ 𝑦 ∈ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) )
29 vex ⊢ 𝑥 ∈ V
30 29 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → 𝑥 ∈ V )
31 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) )
32 elpredg ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → ( 𝑦 ∈ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) ↔ 𝑦 𝑅 𝑥 ) )
33 30 31 32 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → ( 𝑦 ∈ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) ↔ 𝑦 𝑅 𝑥 ) )
34 28 33 mtbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → ¬ 𝑦 𝑅 𝑥 )
35 34 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ) ∧ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ) → ¬ 𝑦 𝑅 𝑥 )
36 35 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) ) → ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 )
37 36 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ → ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 ) )
38 simp1rl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐴 )
39 simp1rr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ◡ 𝑅 𝑋 )
40 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) → 𝑋 ∈ 𝑉 )
41 40 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑋 ∈ 𝑉 )
42 29 elpred ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑥 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) )
43 41 42 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → ( 𝑥 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) )
44 38 39 43 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) )
45 simp3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 𝑅 𝑦 )
46 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝑅 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
47 46 rspcev ⊢ ( ( 𝑥 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 )
48 44 45 47 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 )
49 48 3expia ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) )
50 49 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ◡ 𝑅 𝑋 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) )
51 50 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ◡ 𝑅 𝑋 → ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) ) )
52 37 51 anim12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ∧ 𝑥 ◡ 𝑅 𝑋 ) → ( ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) ) ) )
53 52 ancomsd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ◡ 𝑅 𝑋 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) → ( ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) ) ) )
54 53 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 ◡ 𝑅 𝑋 ∧ Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) ) ) )
55 24 54 syl5bi ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ◡ 𝑅 𝑋 } Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) ) ) )
56 22 55 sylbid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) Pred ( 𝑅 , Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝑥 ) = ∅ → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) ) ) )
57 19 56 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑧 𝑅 𝑦 ) ) )