Metamath Proof Explorer

Theorem ttrclselem1

Description: Lemma for ttrclse . Show that all finite ordinal function values of F are subsets of A . (Contributed by Scott Fenton, 31-Oct-2024)

Ref Expression
Hypothesis ttrclselem.1 ⊢ 𝐹 = rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) )
Assertion ttrclselem1 ( 𝑁 ∈ ω → ( 𝐹 ‘ 𝑁 ) ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 ttrclselem.1 ⊢ 𝐹 = rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) )
2 nn0suc ⊢ ( 𝑁 ∈ ω → ( 𝑁 = ∅ ∨ ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 ) )
3 1 fveq1i ⊢ ( 𝐹 ‘ 𝑁 ) = ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ 𝑁 )
4 fveq2 ⊢ ( 𝑁 = ∅ → ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ 𝑁 ) = ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ ∅ ) )
5 3 4 eqtrid ⊢ ( 𝑁 = ∅ → ( 𝐹 ‘ 𝑁 ) = ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ ∅ ) )
6 rdg0g ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ ∅ ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
7 predss ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴
8 6 7 eqsstrdi ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ ∅ ) ⊆ 𝐴 )
9 rdg0n ⊢ ( ¬ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ ∅ ) = ∅ )
10 0ss ⊢ ∅ ⊆ 𝐴
11 9 10 eqsstrdi ⊢ ( ¬ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∈ V → ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ ∅ ) ⊆ 𝐴 )
12 8 11 pm2.61i ⊢ ( rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ‘ ∅ ) ⊆ 𝐴
13 5 12 eqsstrdi ⊢ ( 𝑁 = ∅ → ( 𝐹 ‘ 𝑁 ) ⊆ 𝐴 )
14 nnon ⊢ ( 𝑛 ∈ ω → 𝑛 ∈ On )
15 nfcv ⊢ Ⅎ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑋 )
16 nfcv ⊢ Ⅎ 𝑏 𝑛
17 nfmpt1 ⊢ Ⅎ 𝑏 ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) )
18 17 15 nfrdg ⊢ Ⅎ 𝑏 rec ( ( 𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) ) , Pred ( 𝑅 , 𝐴 , 𝑋 ) )
19 1 18 nfcxfr ⊢ Ⅎ 𝑏 𝐹
20 19 16 nffv ⊢ Ⅎ 𝑏 ( 𝐹 ‘ 𝑛 )
21 nfcv ⊢ Ⅎ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑡 )
22 20 21 nfiun ⊢ Ⅎ 𝑏 ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 )
23 predeq3 ⊢ ( 𝑤 = 𝑡 → Pred ( 𝑅 , 𝐴 , 𝑤 ) = Pred ( 𝑅 , 𝐴 , 𝑡 ) )
24 23 cbviunv ⊢ ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) = ∪ 𝑡 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑡 )
25 iuneq1 ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑛 ) → ∪ 𝑡 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑡 ) = ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
26 24 25 eqtrid ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑛 ) → ∪ 𝑤 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑤 ) = ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
27 15 16 22 1 26 rdgsucmptf ⊢ ( ( 𝑛 ∈ On ∧ ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) → ( 𝐹 ‘ suc 𝑛 ) = ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) )
28 iunss ⊢ ( ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ⊆ 𝐴 ↔ ∀ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ⊆ 𝐴 )
29 predss ⊢ Pred ( 𝑅 , 𝐴 , 𝑡 ) ⊆ 𝐴
30 29 a1i ⊢ ( 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) → Pred ( 𝑅 , 𝐴 , 𝑡 ) ⊆ 𝐴 )
31 28 30 mprgbir ⊢ ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ⊆ 𝐴
32 27 31 eqsstrdi ⊢ ( ( 𝑛 ∈ On ∧ ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) → ( 𝐹 ‘ suc 𝑛 ) ⊆ 𝐴 )
33 14 32 sylan ⊢ ( ( 𝑛 ∈ ω ∧ ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) → ( 𝐹 ‘ suc 𝑛 ) ⊆ 𝐴 )
34 15 16 22 1 26 rdgsucmptnf ⊢ ( ¬ ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V → ( 𝐹 ‘ suc 𝑛 ) = ∅ )
35 34 10 eqsstrdi ⊢ ( ¬ ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V → ( 𝐹 ‘ suc 𝑛 ) ⊆ 𝐴 )
36 35 adantl ⊢ ( ( 𝑛 ∈ ω ∧ ¬ ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) Pred ( 𝑅 , 𝐴 , 𝑡 ) ∈ V ) → ( 𝐹 ‘ suc 𝑛 ) ⊆ 𝐴 )
37 33 36 pm2.61dan ⊢ ( 𝑛 ∈ ω → ( 𝐹 ‘ suc 𝑛 ) ⊆ 𝐴 )
38 fveq2 ⊢ ( 𝑁 = suc 𝑛 → ( 𝐹 ‘ 𝑁 ) = ( 𝐹 ‘ suc 𝑛 ) )
39 38 sseq1d ⊢ ( 𝑁 = suc 𝑛 → ( ( 𝐹 ‘ 𝑁 ) ⊆ 𝐴 ↔ ( 𝐹 ‘ suc 𝑛 ) ⊆ 𝐴 ) )
40 37 39 syl5ibrcom ⊢ ( 𝑛 ∈ ω → ( 𝑁 = suc 𝑛 → ( 𝐹 ‘ 𝑁 ) ⊆ 𝐴 ) )
41 40 rexlimiv ⊢ ( ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 → ( 𝐹 ‘ 𝑁 ) ⊆ 𝐴 )
42 13 41 jaoi ⊢ ( ( 𝑁 = ∅ ∨ ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 ) → ( 𝐹 ‘ 𝑁 ) ⊆ 𝐴 )
43 2 42 syl ⊢ ( 𝑁 ∈ ω → ( 𝐹 ‘ 𝑁 ) ⊆ 𝐴 )