This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1204

Description: Well-founded induction. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1204.1 ⊢ ( 𝜓 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) )
Assertion bnj1204 ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 bnj1204.1 ⊢ ( 𝜓 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) )
2 simp1 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) → 𝑅 FrSe 𝐴 )
3 ssrab2 ⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ⊆ 𝐴
4 3 a1i ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) → { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ⊆ 𝐴 )
5 simp3 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) → ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 )
6 rabn0 ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 )
7 5 6 sylibr ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) → { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ )
8 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }
9 8 nfcrii ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → ∀ 𝑥 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } )
10 9 bnj1228 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 )
11 2 4 7 10 syl3anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) → ∃ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 )
12 biid ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) )
13 nfv ⊢ Ⅎ 𝑥 𝑅 FrSe 𝐴
14 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 )
15 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 ¬ 𝜑
16 13 14 15 nf3an ⊢ Ⅎ 𝑥 ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 )
17 16 nf5ri ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) → ∀ 𝑥 ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) )
18 11 12 17 bnj1521 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) → ∃ 𝑥 ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) )
19 eqid ⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }
20 19 12 bnj1212 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → 𝑥 ∈ 𝐴 )
21 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥
22 simp3 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 )
23 22 bnj1211 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → ¬ 𝑦 𝑅 𝑥 ) )
24 con2b ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → ¬ 𝑦 𝑅 𝑥 ) ↔ ( 𝑦 𝑅 𝑥 → ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) )
25 24 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → ¬ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) )
26 23 25 sylib ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) )
27 simp2 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → 𝑦 𝑅 𝑥 )
28 sp ⊢ ( ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) → ( 𝑦 𝑅 𝑥 → ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ) )
29 26 27 28 sylc ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } )
30 simp1 ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → 𝑦 ∈ 𝐴 )
31 nfcv ⊢ Ⅎ 𝑥 𝐴
32 31 elrabsf ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ↔ ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
33 vex ⊢ 𝑦 ∈ V
34 sbcng ⊢ ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑦 / 𝑥 ] 𝜑 ) )
35 33 34 ax-mp ⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑦 / 𝑥 ] 𝜑 )
36 35 anbi2i ⊢ ( ( 𝑦 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ [ 𝑦 / 𝑥 ] 𝜑 ) )
37 32 36 bitri ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ [ 𝑦 / 𝑥 ] 𝜑 ) )
38 37 notbii ⊢ ( ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ↔ ¬ ( 𝑦 ∈ 𝐴 ∧ ¬ [ 𝑦 / 𝑥 ] 𝜑 ) )
39 imnan ⊢ ( ( 𝑦 ∈ 𝐴 → ¬ ¬ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ¬ ( 𝑦 ∈ 𝐴 ∧ ¬ [ 𝑦 / 𝑥 ] 𝜑 ) )
40 38 39 sylbb2 ⊢ ( ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → ( 𝑦 ∈ 𝐴 → ¬ ¬ [ 𝑦 / 𝑥 ] 𝜑 ) )
41 40 imp ⊢ ( ( ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ 𝑦 ∈ 𝐴 ) → ¬ ¬ [ 𝑦 / 𝑥 ] 𝜑 )
42 41 notnotrd ⊢ ( ( ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ 𝑦 ∈ 𝐴 ) → [ 𝑦 / 𝑥 ] 𝜑 )
43 29 30 42 syl2anc ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → [ 𝑦 / 𝑥 ] 𝜑 )
44 43 3expa ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → [ 𝑦 / 𝑥 ] 𝜑 )
45 44 expcom ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 → ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 𝑅 𝑥 ) → [ 𝑦 / 𝑥 ] 𝜑 ) )
46 45 expd ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 → ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
47 21 46 ralrimi ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) )
48 47 1 sylibr ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 → 𝜓 )
49 48 3ad2ant3 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → 𝜓 )
50 simp12 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) )
51 simp3 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) )
52 51 bnj1211 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜑 ) ) )
53 simp1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → 𝑥 ∈ 𝐴 )
54 simp2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → 𝜓 )
55 sp ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜑 ) ) → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜑 ) ) )
56 52 53 54 55 syl3c ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → 𝜑 )
57 20 49 50 56 syl3anc ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → 𝜑 )
58 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) )
59 58 simprbi ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → ¬ 𝜑 )
60 59 3ad2ant2 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ) ∧ 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑦 𝑅 𝑥 ) → ¬ 𝜑 )
61 18 57 60 bnj1304 ⊢ ¬ ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 )
62 61 bnj1224 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 )
63 dfral2 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 )
64 62 63 sylibr ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 𝜑 )