Metamath Proof Explorer

Theorem rdgssun

Description: In a recursive definition where each step expands on the previous one using a union, every previous step is a subset of every later step. (Contributed by ML, 1-Apr-2022)

Ref Expression
Hypotheses rdgssun.1 ⊢ 𝐹 = ( 𝑤 ∈ V ↦ ( 𝑤 ∪ 𝐵 ) )
rdgssun.2 ⊢ 𝐵 ∈ V
Assertion rdgssun ( ( 𝑋 ∈ On ∧ 𝑌 ∈ 𝑋 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 rdgssun.1 ⊢ 𝐹 = ( 𝑤 ∈ V ↦ ( 𝑤 ∪ 𝐵 ) )
2 rdgssun.2 ⊢ 𝐵 ∈ V
3 nfsbc1v ⊢ Ⅎ 𝑥 [ ∅ / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 )
4 0ex ⊢ ∅ ∈ V
5 rzal ⊢ ( 𝑥 = ∅ → ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )
6 sbceq1a ⊢ ( 𝑥 = ∅ → ( ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ [ ∅ / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) )
7 5 6 mpbid ⊢ ( 𝑥 = ∅ → [ ∅ / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )
8 3 4 7 vtoclef ⊢ [ ∅ / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 )
9 vex ⊢ 𝑦 ∈ V
10 9 elsuc ⊢ ( 𝑦 ∈ suc 𝑥 ↔ ( 𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ) )
11 ssun1 ⊢ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ⊆ ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∪ ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 )
12 fvex ⊢ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∈ V
13 2 csbex ⊢ ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 ∈ V
14 12 13 unex ⊢ ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∪ ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 ) ∈ V
15 nfcv ⊢ Ⅎ 𝑤 𝐴
16 nfcv ⊢ Ⅎ 𝑤 𝑥
17 nfmpt1 ⊢ Ⅎ 𝑤 ( 𝑤 ∈ V ↦ ( 𝑤 ∪ 𝐵 ) )
18 1 17 nfcxfr ⊢ Ⅎ 𝑤 𝐹
19 18 15 nfrdg ⊢ Ⅎ 𝑤 rec ( 𝐹 , 𝐴 )
20 19 16 nffv ⊢ Ⅎ 𝑤 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 )
21 20 nfcsb1 ⊢ Ⅎ 𝑤 ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵
22 20 21 nfun ⊢ Ⅎ 𝑤 ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∪ ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 )
23 rdgeq1 ⊢ ( 𝐹 = ( 𝑤 ∈ V ↦ ( 𝑤 ∪ 𝐵 ) ) → rec ( 𝐹 , 𝐴 ) = rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ 𝐵 ) ) , 𝐴 ) )
24 1 23 ax-mp ⊢ rec ( 𝐹 , 𝐴 ) = rec ( ( 𝑤 ∈ V ↦ ( 𝑤 ∪ 𝐵 ) ) , 𝐴 )
25 id ⊢ ( 𝑤 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → 𝑤 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )
26 csbeq1a ⊢ ( 𝑤 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → 𝐵 = ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 )
27 25 26 uneq12d ⊢ ( 𝑤 = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → ( 𝑤 ∪ 𝐵 ) = ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∪ ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 ) )
28 15 16 22 24 27 rdgsucmptf ⊢ ( ( 𝑥 ∈ On ∧ ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∪ ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 ) ∈ V ) → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) = ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∪ ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 ) )
29 14 28 mpan2 ⊢ ( 𝑥 ∈ On → ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) = ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ∪ ⦋ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) / 𝑤 ⦌ 𝐵 ) )
30 11 29 sseqtrrid ⊢ ( 𝑥 ∈ On → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) )
31 sstr2 ⊢ ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
32 30 31 syl5com ⊢ ( 𝑥 ∈ On → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
33 32 imim2d ⊢ ( 𝑥 ∈ On → ( ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) ) )
34 33 imp ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) ) → ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
35 fveq2 ⊢ ( 𝑦 = 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )
36 35 sseq1d ⊢ ( 𝑦 = 𝑥 → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ↔ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
37 30 36 syl5ibrcom ⊢ ( 𝑥 ∈ On → ( 𝑦 = 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
38 37 adantr ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) ) → ( 𝑦 = 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
39 34 38 jaod ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) ) → ( ( 𝑦 ∈ 𝑥 ∨ 𝑦 = 𝑥 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
40 10 39 syl5bi ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) ) → ( 𝑦 ∈ suc 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
41 40 ex ⊢ ( 𝑥 ∈ On → ( ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) → ( 𝑦 ∈ suc 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) ) )
42 41 ralimdv2 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → ∀ 𝑦 ∈ suc 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
43 df-sbc ⊢ ( [ suc 𝑥 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ suc 𝑥 ∈ { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )
44 vex ⊢ 𝑥 ∈ V
45 44 sucex ⊢ suc 𝑥 ∈ V
46 fveq2 ⊢ ( 𝑧 = suc 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) = ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) )
47 46 sseq2d ⊢ ( 𝑧 = suc 𝑥 → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) ↔ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
48 47 raleqbi1dv ⊢ ( 𝑧 = suc 𝑥 → ( ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) ↔ ∀ 𝑦 ∈ suc 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) ) )
49 fveq2 ⊢ ( 𝑥 = 𝑧 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) )
50 49 sseq2d ⊢ ( 𝑥 = 𝑧 → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) ) )
51 50 raleqbi1dv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) ) )
52 51 cbvabv ⊢ { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } = { 𝑧 ∣ ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) }
53 45 48 52 elab2 ⊢ ( suc 𝑥 ∈ { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } ↔ ∀ 𝑦 ∈ suc 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) )
54 43 53 bitri ⊢ ( [ suc 𝑥 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ suc 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ suc 𝑥 ) )
55 42 54 syl6ibr ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → [ suc 𝑥 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) )
56 ssiun2 ⊢ ( 𝑦 ∈ 𝑧 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) )
57 56 adantl ⊢ ( ( Lim 𝑧 ∧ 𝑦 ∈ 𝑧 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ∪ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) )
58 vex ⊢ 𝑧 ∈ V
59 rdglim2a ⊢ ( ( 𝑧 ∈ V ∧ Lim 𝑧 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) = ∪ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) )
60 58 59 mpan ⊢ ( Lim 𝑧 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) = ∪ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) )
61 60 adantr ⊢ ( ( Lim 𝑧 ∧ 𝑦 ∈ 𝑧 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) = ∪ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) )
62 57 61 sseqtrrd ⊢ ( ( Lim 𝑧 ∧ 𝑦 ∈ 𝑧 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) )
63 62 ralrimiva ⊢ ( Lim 𝑧 → ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) )
64 df-sbc ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ 𝑧 ∈ { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } )
65 52 eleq2i ⊢ ( 𝑧 ∈ { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) } ↔ 𝑧 ∈ { 𝑧 ∣ ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) } )
66 64 65 bitri ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ 𝑧 ∈ { 𝑧 ∣ ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) } )
67 abid ⊢ ( 𝑧 ∈ { 𝑧 ∣ ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) } ↔ ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) )
68 66 67 bitri ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑧 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑧 ) )
69 63 68 sylibr ⊢ ( Lim 𝑧 → [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )
70 69 a1d ⊢ ( Lim 𝑧 → ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) )
71 8 55 70 tfindes ⊢ ( 𝑥 ∈ On → ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) )
72 rsp ⊢ ( ∀ 𝑦 ∈ 𝑥 ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) → ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) )
73 71 72 syl ⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) )
74 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ On ↔ 𝑋 ∈ On ) )
75 74 adantl ⊢ ( ( 𝑦 = 𝑌 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ∈ On ↔ 𝑋 ∈ On ) )
76 eleq12 ⊢ ( ( 𝑦 = 𝑌 ∧ 𝑥 = 𝑋 ) → ( 𝑦 ∈ 𝑥 ↔ 𝑌 ∈ 𝑋 ) )
77 fveq2 ⊢ ( 𝑦 = 𝑌 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) )
78 77 adantr ⊢ ( ( 𝑦 = 𝑌 ∧ 𝑥 = 𝑋 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) )
79 fveq2 ⊢ ( 𝑥 = 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) )
80 79 adantl ⊢ ( ( 𝑦 = 𝑌 ∧ 𝑥 = 𝑋 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) = ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) )
81 78 80 sseq12d ⊢ ( ( 𝑦 = 𝑌 ∧ 𝑥 = 𝑋 ) → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ↔ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) )
82 76 81 imbi12d ⊢ ( ( 𝑦 = 𝑌 ∧ 𝑥 = 𝑋 ) → ( ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) ↔ ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) ) )
83 75 82 imbi12d ⊢ ( ( 𝑦 = 𝑌 ∧ 𝑥 = 𝑋 ) → ( ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑦 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑥 ) ) ) ↔ ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) ) ) )
84 73 83 mpbii ⊢ ( ( 𝑦 = 𝑌 ∧ 𝑥 = 𝑋 ) → ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) ) )
85 84 ex ⊢ ( 𝑦 = 𝑌 → ( 𝑥 = 𝑋 → ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) ) ) )
86 85 vtocleg ⊢ ( 𝑌 ∈ 𝑋 → ( 𝑥 = 𝑋 → ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) ) ) )
87 86 com12 ⊢ ( 𝑥 = 𝑋 → ( 𝑌 ∈ 𝑋 → ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) ) ) )
88 87 vtocleg ⊢ ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) ) ) )
89 88 pm2.43b ⊢ ( 𝑌 ∈ 𝑋 → ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) ) )
90 89 pm2.43b ⊢ ( 𝑋 ∈ On → ( 𝑌 ∈ 𝑋 → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) ) )
91 90 imp ⊢ ( ( 𝑋 ∈ On ∧ 𝑌 ∈ 𝑋 ) → ( rec ( 𝐹 , 𝐴 ) ‘ 𝑌 ) ⊆ ( rec ( 𝐹 , 𝐴 ) ‘ 𝑋 ) )