Metamath Proof Explorer


Theorem wzel

Description: The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018) (Revised by AV, 10-Oct-2021)

Ref Expression
Assertion wzel ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → inf ( 𝐴 , 𝐴 , 𝑅 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 weso ( 𝑅 We 𝐴𝑅 Or 𝐴 )
2 1 3ad2ant1 ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → 𝑅 Or 𝐴 )
3 simp1 ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → 𝑅 We 𝐴 )
4 simp2 ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → 𝑅 Se 𝐴 )
5 ssidd ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → 𝐴𝐴 )
6 simp3 ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
7 tz6.26 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐴𝐴𝐴 ≠ ∅ ) ) → ∃ 𝑥𝐴 Pred ( 𝑅 , 𝐴 , 𝑥 ) = ∅ )
8 3 4 5 6 7 syl22anc ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → ∃ 𝑥𝐴 Pred ( 𝑅 , 𝐴 , 𝑥 ) = ∅ )
9 vex 𝑦 ∈ V
10 9 elpred ( 𝑥 ∈ V → ( 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) ↔ ( 𝑦𝐴𝑦 𝑅 𝑥 ) ) )
11 10 elv ( 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) ↔ ( 𝑦𝐴𝑦 𝑅 𝑥 ) )
12 11 notbii ( ¬ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) ↔ ¬ ( 𝑦𝐴𝑦 𝑅 𝑥 ) )
13 imnan ( ( 𝑦𝐴 → ¬ 𝑦 𝑅 𝑥 ) ↔ ¬ ( 𝑦𝐴𝑦 𝑅 𝑥 ) )
14 12 13 bitr4i ( ¬ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) ↔ ( 𝑦𝐴 → ¬ 𝑦 𝑅 𝑥 ) )
15 pm2.27 ( 𝑦𝐴 → ( ( 𝑦𝐴 → ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑦 𝑅 𝑥 ) )
16 15 ad2antll ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝑦𝐴 → ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑦 𝑅 𝑥 ) )
17 breq1 ( 𝑧 = 𝑥 → ( 𝑧 𝑅 𝑦𝑥 𝑅 𝑦 ) )
18 17 rspcev ( ( 𝑥𝐴𝑥 𝑅 𝑦 ) → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 )
19 18 ex ( 𝑥𝐴 → ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) )
20 19 ad2antrl ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) )
21 16 20 jctird ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ( 𝑦𝐴 → ¬ 𝑦 𝑅 𝑥 ) → ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) )
22 14 21 syl5bi ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) ∧ ( 𝑥𝐴𝑦𝐴 ) ) → ( ¬ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) → ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) )
23 22 expr ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → ( 𝑦𝐴 → ( ¬ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) → ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) ) )
24 23 com23 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → ( ¬ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) → ( 𝑦𝐴 → ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) ) )
25 24 alimdv ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → ( ∀ 𝑦 ¬ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) → ∀ 𝑦 ( 𝑦𝐴 → ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) ) )
26 eq0 ( Pred ( 𝑅 , 𝐴 , 𝑥 ) = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑥 ) )
27 r19.26 ( ∀ 𝑦𝐴 ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ↔ ( ∀ 𝑦𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) )
28 df-ral ( ∀ 𝑦𝐴 ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦𝐴 → ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) )
29 27 28 bitr3i ( ( ∀ 𝑦𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦𝐴 → ( ¬ 𝑦 𝑅 𝑥 ∧ ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) )
30 25 26 29 3imtr4g ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) ∧ 𝑥𝐴 ) → ( Pred ( 𝑅 , 𝐴 , 𝑥 ) = ∅ → ( ∀ 𝑦𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) )
31 30 reximdva ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → ( ∃ 𝑥𝐴 Pred ( 𝑅 , 𝐴 , 𝑥 ) = ∅ → ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) ) )
32 8 31 mpd ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → ∃ 𝑥𝐴 ( ∀ 𝑦𝐴 ¬ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦𝐴 ( 𝑥 𝑅 𝑦 → ∃ 𝑧𝐴 𝑧 𝑅 𝑦 ) ) )
33 2 32 infcl ( ( 𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅ ) → inf ( 𝐴 , 𝐴 , 𝑅 ) ∈ 𝐴 )