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	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
	bnj60.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
	bnj60.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
	bnj60.4	⊢ 𝐹 = ∪ 𝐶
Assertion	bnj60	⊢ ( 𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bnj60.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2		bnj60.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3		bnj60.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4		bnj60.4	⊢ 𝐹 = ∪ 𝐶
5	1 2 3	bnj1497	⊢ ∀ 𝑔 ∈ 𝐶 Fun 𝑔
6		eqid	⊢ ( dom 𝑔 ∩ dom ℎ ) = ( dom 𝑔 ∩ dom ℎ )
7	1 2 3 6	bnj1311	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ) → ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) = ( ℎ ↾ ( dom 𝑔 ∩ dom ℎ ) ) )
8	7	3expia	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ) → ( ℎ ∈ 𝐶 → ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) = ( ℎ ↾ ( dom 𝑔 ∩ dom ℎ ) ) ) )
9	8	ralrimiv	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ) → ∀ ℎ ∈ 𝐶 ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) = ( ℎ ↾ ( dom 𝑔 ∩ dom ℎ ) ) )
10	9	ralrimiva	⊢ ( 𝑅 FrSe 𝐴 → ∀ 𝑔 ∈ 𝐶 ∀ ℎ ∈ 𝐶 ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) = ( ℎ ↾ ( dom 𝑔 ∩ dom ℎ ) ) )
11		biid	⊢ ( ∀ 𝑔 ∈ 𝐶 Fun 𝑔 ↔ ∀ 𝑔 ∈ 𝐶 Fun 𝑔 )
12		biid	⊢ ( ( ∀ 𝑔 ∈ 𝐶 Fun 𝑔 ∧ ∀ 𝑔 ∈ 𝐶 ∀ ℎ ∈ 𝐶 ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) = ( ℎ ↾ ( dom 𝑔 ∩ dom ℎ ) ) ) ↔ ( ∀ 𝑔 ∈ 𝐶 Fun 𝑔 ∧ ∀ 𝑔 ∈ 𝐶 ∀ ℎ ∈ 𝐶 ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) = ( ℎ ↾ ( dom 𝑔 ∩ dom ℎ ) ) ) )
13	11 6 12	bnj1383	⊢ ( ( ∀ 𝑔 ∈ 𝐶 Fun 𝑔 ∧ ∀ 𝑔 ∈ 𝐶 ∀ ℎ ∈ 𝐶 ( 𝑔 ↾ ( dom 𝑔 ∩ dom ℎ ) ) = ( ℎ ↾ ( dom 𝑔 ∩ dom ℎ ) ) ) → Fun ∪ 𝐶 )
14	5 10 13	sylancr	⊢ ( 𝑅 FrSe 𝐴 → Fun ∪ 𝐶 )
15	4	funeqi	⊢ ( Fun 𝐹 ↔ Fun ∪ 𝐶 )
16	14 15	sylibr	⊢ ( 𝑅 FrSe 𝐴 → Fun 𝐹 )
17	1 2 3 4	bnj1498	⊢ ( 𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴 )
18	16 17	bnj1422	⊢ ( 𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴 )