This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1463

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1463.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1463.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1463.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1463.4 ⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
bnj1463.5 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
bnj1463.6 ⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
bnj1463.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
bnj1463.8 ⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
bnj1463.9 ⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
bnj1463.10 ⊢ 𝑃 = ∪ 𝐻
bnj1463.11 ⊢ 𝑍 = ⟨ 𝑥 , ( 𝑃 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1463.12 ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ 𝑍 ) ⟩ } )
bnj1463.13 ⊢ 𝑊 = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
bnj1463.14 ⊢ 𝐸 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
bnj1463.15 ⊢ ( 𝜒 → 𝑄 ∈ V )
bnj1463.16 ⊢ ( 𝜒 → ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
bnj1463.17 ⊢ ( 𝜒 → 𝑄 Fn 𝐸 )
bnj1463.18 ⊢ ( 𝜒 → 𝐸 ∈ 𝐵 )
Assertion bnj1463 ( 𝜒 → 𝑄 ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 bnj1463.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1463.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1463.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1463.4 ⊢ ( 𝜏 ↔ ( 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) ) )
5 bnj1463.5 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ¬ ∃ 𝑓 𝜏 }
6 bnj1463.6 ⊢ ( 𝜓 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅ ) )
7 bnj1463.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀ 𝑦 ∈ 𝐷 ¬ 𝑦 𝑅 𝑥 ) )
8 bnj1463.8 ⊢ ( 𝜏′ ↔ [ 𝑦 / 𝑥 ] 𝜏 )
9 bnj1463.9 ⊢ 𝐻 = { 𝑓 ∣ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝜏′ }
10 bnj1463.10 ⊢ 𝑃 = ∪ 𝐻
11 bnj1463.11 ⊢ 𝑍 = ⟨ 𝑥 , ( 𝑃 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
12 bnj1463.12 ⊢ 𝑄 = ( 𝑃 ∪ { ⟨ 𝑥 , ( 𝐺 ‘ 𝑍 ) ⟩ } )
13 bnj1463.13 ⊢ 𝑊 = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩
14 bnj1463.14 ⊢ 𝐸 = ( { 𝑥 } ∪ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
15 bnj1463.15 ⊢ ( 𝜒 → 𝑄 ∈ V )
16 bnj1463.16 ⊢ ( 𝜒 → ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
17 bnj1463.17 ⊢ ( 𝜒 → 𝑄 Fn 𝐸 )
18 bnj1463.18 ⊢ ( 𝜒 → 𝐸 ∈ 𝐵 )
19 18 elexd ⊢ ( 𝜒 → 𝐸 ∈ V )
20 eleq1 ⊢ ( 𝑑 = 𝐸 → ( 𝑑 ∈ 𝐵 ↔ 𝐸 ∈ 𝐵 ) )
21 fneq2 ⊢ ( 𝑑 = 𝐸 → ( 𝑄 Fn 𝑑 ↔ 𝑄 Fn 𝐸 ) )
22 raleq ⊢ ( 𝑑 = 𝐸 → ( ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ↔ ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) )
23 21 22 anbi12d ⊢ ( 𝑑 = 𝐸 → ( ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ↔ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
24 20 23 anbi12d ⊢ ( 𝑑 = 𝐸 → ( ( 𝑑 ∈ 𝐵 ∧ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) ↔ ( 𝐸 ∈ 𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) ) )
25 1 bnj1317 ⊢ ( 𝑤 ∈ 𝐵 → ∀ 𝑑 𝑤 ∈ 𝐵 )
26 25 nfcii ⊢ Ⅎ 𝑑 𝐵
27 26 nfel2 ⊢ Ⅎ 𝑑 𝐸 ∈ 𝐵
28 1 2 3 4 5 6 7 8 9 10 11 12 bnj1467 ⊢ ( 𝑤 ∈ 𝑄 → ∀ 𝑑 𝑤 ∈ 𝑄 )
29 28 nfcii ⊢ Ⅎ 𝑑 𝑄
30 nfcv ⊢ Ⅎ 𝑑 𝐸
31 29 30 nffn ⊢ Ⅎ 𝑑 𝑄 Fn 𝐸
32 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1446 ⊢ ( ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) → ∀ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
33 32 nf5i ⊢ Ⅎ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 )
34 30 33 nfralw ⊢ Ⅎ 𝑑 ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 )
35 31 34 nfan ⊢ Ⅎ 𝑑 ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
36 27 35 nfan ⊢ Ⅎ 𝑑 ( 𝐸 ∈ 𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) )
37 36 nf5ri ⊢ ( ( 𝐸 ∈ 𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) → ∀ 𝑑 ( 𝐸 ∈ 𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
38 18 17 16 jca32 ⊢ ( 𝜒 → ( 𝐸 ∈ 𝐵 ∧ ( 𝑄 Fn 𝐸 ∧ ∀ 𝑧 ∈ 𝐸 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
39 24 37 38 bnj1465 ⊢ ( ( 𝜒 ∧ 𝐸 ∈ V ) → ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
40 19 39 mpdan ⊢ ( 𝜒 → ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
41 df-rex ⊢ ( ∃ 𝑑 ∈ 𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ↔ ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
42 40 41 sylibr ⊢ ( 𝜒 → ∃ 𝑑 ∈ 𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) )
43 nfcv ⊢ Ⅎ 𝑓 𝐵
44 1 2 3 4 5 6 7 8 9 10 11 12 bnj1466 ⊢ ( 𝑤 ∈ 𝑄 → ∀ 𝑓 𝑤 ∈ 𝑄 )
45 44 nfcii ⊢ Ⅎ 𝑓 𝑄
46 nfcv ⊢ Ⅎ 𝑓 𝑑
47 45 46 nffn ⊢ Ⅎ 𝑓 𝑄 Fn 𝑑
48 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1448 ⊢ ( ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) → ∀ 𝑓 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
49 48 nf5i ⊢ Ⅎ 𝑓 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 )
50 46 49 nfralw ⊢ Ⅎ 𝑓 ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 )
51 47 50 nfan ⊢ Ⅎ 𝑓 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
52 43 51 nfrexw ⊢ Ⅎ 𝑓 ∃ 𝑑 ∈ 𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) )
53 52 nf5ri ⊢ ( ∃ 𝑑 ∈ 𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) → ∀ 𝑓 ∃ 𝑑 ∈ 𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) )
54 29 nfeq2 ⊢ Ⅎ 𝑑 𝑓 = 𝑄
55 fneq1 ⊢ ( 𝑓 = 𝑄 → ( 𝑓 Fn 𝑑 ↔ 𝑄 Fn 𝑑 ) )
56 fveq1 ⊢ ( 𝑓 = 𝑄 → ( 𝑓 ‘ 𝑧 ) = ( 𝑄 ‘ 𝑧 ) )
57 reseq1 ⊢ ( 𝑓 = 𝑄 → ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) = ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) )
58 57 opeq2d ⊢ ( 𝑓 = 𝑄 → ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑧 , ( 𝑄 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ )
59 58 13 eqtr4di ⊢ ( 𝑓 = 𝑄 → ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ = 𝑊 )
60 59 fveq2d ⊢ ( 𝑓 = 𝑄 → ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) = ( 𝐺 ‘ 𝑊 ) )
61 56 60 eqeq12d ⊢ ( 𝑓 = 𝑄 → ( ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ↔ ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) )
62 61 ralbidv ⊢ ( 𝑓 = 𝑄 → ( ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ↔ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) )
63 55 62 anbi12d ⊢ ( 𝑓 = 𝑄 → ( ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
64 54 63 rexbid ⊢ ( 𝑓 = 𝑄 → ( ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ∃ 𝑑 ∈ 𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
65 53 64 44 bnj1468 ⊢ ( 𝑄 ∈ V → ( [ 𝑄 / 𝑓 ] ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ∃ 𝑑 ∈ 𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
66 15 65 syl ⊢ ( 𝜒 → ( [ 𝑄 / 𝑓 ] ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) ↔ ∃ 𝑑 ∈ 𝐵 ( 𝑄 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑄 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑊 ) ) ) )
67 42 66 mpbird ⊢ ( 𝜒 → [ 𝑄 / 𝑓 ] ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
68 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑧 ) )
69 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
70 bnj602 ⊢ ( 𝑥 = 𝑧 → pred ( 𝑥 , 𝐴 , 𝑅 ) = pred ( 𝑧 , 𝐴 , 𝑅 ) )
71 70 reseq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) )
72 69 71 opeq12d ⊢ ( 𝑥 = 𝑧 → ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ )
73 2 72 eqtrid ⊢ ( 𝑥 = 𝑧 → 𝑌 = ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ )
74 73 fveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐺 ‘ 𝑌 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) )
75 68 74 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ↔ ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
76 75 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ↔ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) )
77 76 anbi2i ⊢ ( ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ↔ ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
78 77 rexbii ⊢ ( ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ↔ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
79 78 sbcbii ⊢ ( [ 𝑄 / 𝑓 ] ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ↔ [ 𝑄 / 𝑓 ] ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑧 ∈ 𝑑 ( 𝑓 ‘ 𝑧 ) = ( 𝐺 ‘ ⟨ 𝑧 , ( 𝑓 ↾ pred ( 𝑧 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
80 67 79 sylibr ⊢ ( 𝜒 → [ 𝑄 / 𝑓 ] ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) )
81 3 bnj1454 ⊢ ( 𝑄 ∈ V → ( 𝑄 ∈ 𝐶 ↔ [ 𝑄 / 𝑓 ] ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ) )
82 15 81 syl ⊢ ( 𝜒 → ( 𝑄 ∈ 𝐶 ↔ [ 𝑄 / 𝑓 ] ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ) )
83 80 82 mpbird ⊢ ( 𝜒 → 𝑄 ∈ 𝐶 )