Metamath Proof Explorer

Theorem bnj110

Description: Well-founded induction restricted to a set ( A e. _V ). 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
Hypotheses bnj110.1 ⊢ 𝐴 ∈ V
bnj110.2 ⊢ ( 𝜓 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) )
Assertion bnj110 ( ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 bnj110.1 ⊢ 𝐴 ∈ V
2 bnj110.2 ⊢ ( 𝜓 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) )
3 ralnex ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ [ 𝑧 / 𝑥 ] 𝜑 ↔ ¬ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜑 )
4 sbcng ⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑧 / 𝑥 ] 𝜑 ) )
5 4 elv ⊢ ( [ 𝑧 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑧 / 𝑥 ] 𝜑 )
6 5 bicomi ⊢ ( ¬ [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] ¬ 𝜑 )
7 6 ralbii ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] ¬ 𝜑 )
8 3 7 bitr3i ⊢ ( ¬ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] ¬ 𝜑 )
9 df-rab ⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) }
10 9 eleq2i ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ↔ 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) } )
11 df-sbc ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) ↔ 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) } )
12 sbcan ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] ¬ 𝜑 ) )
13 sbcel1v ⊢ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 )
14 13 anbi1i ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] ¬ 𝜑 ) ↔ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] ¬ 𝜑 ) )
15 12 14 bitri ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) ↔ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] ¬ 𝜑 ) )
16 11 15 bitr3i ⊢ ( 𝑧 ∈ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝜑 ) } ↔ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] ¬ 𝜑 ) )
17 10 16 bitri ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ↔ ( 𝑧 ∈ 𝐴 ∧ [ 𝑧 / 𝑥 ] ¬ 𝜑 ) )
18 17 simprbi ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → [ 𝑧 / 𝑥 ] ¬ 𝜑 )
19 8 18 mprgbir ⊢ ¬ ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜑
20 1 rabex ⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∈ V
21 20 biantrur ⊢ ( 𝑅 Fr 𝐴 ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∈ V ∧ 𝑅 Fr 𝐴 ) )
22 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 )
23 rabn0 ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 )
24 ssrab2 ⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ⊆ 𝐴
25 24 biantrur ⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ ) )
26 23 25 bitr3i ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ ) )
27 22 26 bitr3i ⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ ) )
28 fri ⊢ ( ( ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ⊆ 𝐴 ∧ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ≠ ∅ ) ) → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑤 𝑅 𝑧 )
29 21 27 28 syl2anb ⊢ ( ( 𝑅 Fr 𝐴 ∧ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑤 𝑅 𝑧 )
30 eqid ⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } = { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 }
31 30 bnj23 ⊢ ( ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑤 𝑅 𝑧 → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) )
32 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
33 32 sbcbii ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ [ 𝑧 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
34 sbcal ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ∀ 𝑦 [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
35 sbcimg ⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐴 → [ 𝑧 / 𝑥 ] ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) ) )
36 35 elv ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐴 → [ 𝑧 / 𝑥 ] ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
37 vex ⊢ 𝑧 ∈ V
38 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
39 37 38 sbcgfi ⊢ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 )
40 sbcimg ⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑥 ] ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑦 𝑅 𝑥 → [ 𝑧 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ) ) )
41 40 elv ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑦 𝑅 𝑥 → [ 𝑧 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
42 sbcbr2g ⊢ ( 𝑧 ∈ V → ( [ 𝑧 / 𝑥 ] 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑥 ) )
43 42 elv ⊢ ( [ 𝑧 / 𝑥 ] 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑥 )
44 37 csbvargi ⊢ ⦋ 𝑧 / 𝑥 ⦌ 𝑥 = 𝑧
45 44 breq2i ⊢ ( 𝑦 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑥 ↔ 𝑦 𝑅 𝑧 )
46 43 45 bitri ⊢ ( [ 𝑧 / 𝑥 ] 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑧 )
47 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
48 37 47 sbcgfi ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
49 46 48 imbi12i ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑦 𝑅 𝑥 → [ 𝑧 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) )
50 41 49 bitri ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) )
51 39 50 imbi12i ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝐴 → [ 𝑧 / 𝑥 ] ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
52 36 51 bitri ⊢ ( [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
53 52 albii ⊢ ( ∀ 𝑦 [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
54 34 53 bitri ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
55 33 54 bitri ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
56 2 sbcbii ⊢ ( [ 𝑧 / 𝑥 ] 𝜓 ↔ [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜑 ) )
57 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
58 55 56 57 3bitr4i ⊢ ( [ 𝑧 / 𝑥 ] 𝜓 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → [ 𝑦 / 𝑥 ] 𝜑 ) )
59 31 58 sylibr ⊢ ( ∀ 𝑤 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ¬ 𝑤 𝑅 𝑧 → [ 𝑧 / 𝑥 ] 𝜓 )
60 29 59 bnj31 ⊢ ( ( 𝑅 Fr 𝐴 ∧ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜓 )
61 nfv ⊢ Ⅎ 𝑧 ( 𝜓 → 𝜑 )
62 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜓
63 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
64 62 63 nfim ⊢ Ⅎ 𝑥 ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 )
65 sbceq1a ⊢ ( 𝑥 = 𝑧 → ( 𝜓 ↔ [ 𝑧 / 𝑥 ] 𝜓 ) )
66 sbceq1a ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
67 65 66 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝜓 → 𝜑 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 ) ) )
68 61 64 67 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐴 ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 ) )
69 elrabi ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → 𝑧 ∈ 𝐴 )
70 69 imim1i ⊢ ( ( 𝑧 ∈ 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 ) ) → ( 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } → ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 ) ) )
71 70 ralimi2 ⊢ ( ∀ 𝑧 ∈ 𝐴 ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 ) → ∀ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 ) )
72 68 71 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) → ∀ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 ) )
73 rexim ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } ( [ 𝑧 / 𝑥 ] 𝜓 → [ 𝑧 / 𝑥 ] 𝜑 ) → ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜓 → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜑 ) )
74 72 73 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) → ( ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜓 → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜑 ) )
75 60 74 mpan9 ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜑 )
76 75 an32s ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑧 ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝜑 } [ 𝑧 / 𝑥 ] 𝜑 )
77 19 76 mto ⊢ ¬ ( ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 )
78 iman ⊢ ( ( ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 𝜑 ) ↔ ¬ ( ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) ∧ ¬ ∀ 𝑥 ∈ 𝐴 𝜑 ) )
79 77 78 mpbir ⊢ ( ( 𝑅 Fr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 𝜑 )