Metamath Proof Explorer

Theorem bnj60

Description: Well-founded recursion, part 1 of 3. 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 bnj60.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj60.2 ⊢ Y = x f ↾ pred x A R
bnj60.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj60.4 ⊢ F = ⋃ C
Assertion bnj60 ⊢ R FrSe A → F Fn A

Proof

Step Hyp Ref Expression
1 bnj60.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj60.2 ⊢ Y = x f ↾ pred x A R
3 bnj60.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj60.4 ⊢ F = ⋃ C
5 1 2 3 bnj1497 ⊢ ∀ g ∈ C Fun ⁡ g
6 eqid ⊢ dom ⁡ g ∩ dom ⁡ h = dom ⁡ g ∩ dom ⁡ h
7 1 2 3 6 bnj1311 ⊢ R FrSe A ∧ g ∈ C ∧ h ∈ C → g ↾ dom ⁡ g ∩ dom ⁡ h = h ↾ dom ⁡ g ∩ dom ⁡ h
8 7 3expia ⊢ R FrSe A ∧ g ∈ C → h ∈ C → g ↾ dom ⁡ g ∩ dom ⁡ h = h ↾ dom ⁡ g ∩ dom ⁡ h
9 8 ralrimiv ⊢ R FrSe A ∧ g ∈ C → ∀ h ∈ C g ↾ dom ⁡ g ∩ dom ⁡ h = h ↾ dom ⁡ g ∩ dom ⁡ h
10 9 ralrimiva ⊢ R FrSe A → ∀ g ∈ C ∀ h ∈ C g ↾ dom ⁡ g ∩ dom ⁡ h = h ↾ dom ⁡ g ∩ dom ⁡ h
11 biid ⊢ ∀ g ∈ C Fun ⁡ g ↔ ∀ g ∈ C Fun ⁡ g
12 biid ⊢ ∀ g ∈ C Fun ⁡ g ∧ ∀ g ∈ C ∀ h ∈ C g ↾ dom ⁡ g ∩ dom ⁡ h = h ↾ dom ⁡ g ∩ dom ⁡ h ↔ ∀ g ∈ C Fun ⁡ g ∧ ∀ g ∈ C ∀ h ∈ C g ↾ dom ⁡ g ∩ dom ⁡ h = h ↾ dom ⁡ g ∩ dom ⁡ h
13 11 6 12 bnj1383 ⊢ ∀ g ∈ C Fun ⁡ g ∧ ∀ g ∈ C ∀ h ∈ C g ↾ dom ⁡ g ∩ dom ⁡ h = h ↾ dom ⁡ g ∩ dom ⁡ h → Fun ⁡ ⋃ C
14 5 10 13 sylancr ⊢ R FrSe A → Fun ⁡ ⋃ C
15 4 funeqi ⊢ Fun ⁡ F ↔ Fun ⁡ ⋃ C
16 14 15 sylibr ⊢ R FrSe A → Fun ⁡ F
17 1 2 3 4 bnj1498 ⊢ R FrSe A → dom ⁡ F = A
18 16 17 bnj1422 ⊢ R FrSe A → F Fn A