Metamath Proof Explorer


Theorem bnj1525

Description: Technical lemma for bnj1522 . 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 bnj1525.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1525.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1525.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
bnj1525.4 𝐹 = 𝐶
bnj1525.5 ( 𝜑 ↔ ( 𝑅 FrSe 𝐴𝐻 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝐻𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
bnj1525.6 ( 𝜓 ↔ ( 𝜑𝐹𝐻 ) )
Assertion bnj1525 ( 𝜓 → ∀ 𝑥 𝜓 )

Proof

Step Hyp Ref Expression
1 bnj1525.1 𝐵 = { 𝑑 ∣ ( 𝑑𝐴 ∧ ∀ 𝑥𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1525.2 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1525.3 𝐶 = { 𝑓 ∣ ∃ 𝑑𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥𝑑 ( 𝑓𝑥 ) = ( 𝐺𝑌 ) ) }
4 bnj1525.4 𝐹 = 𝐶
5 bnj1525.5 ( 𝜑 ↔ ( 𝑅 FrSe 𝐴𝐻 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝐻𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
6 bnj1525.6 ( 𝜓 ↔ ( 𝜑𝐹𝐻 ) )
7 nfv 𝑥 𝑅 FrSe 𝐴
8 nfv 𝑥 𝐻 Fn 𝐴
9 nfra1 𝑥𝑥𝐴 ( 𝐻𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ )
10 7 8 9 nf3an 𝑥 ( 𝑅 FrSe 𝐴𝐻 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝐻𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
11 5 10 nfxfr 𝑥 𝜑
12 1 bnj1309 ( 𝑤𝐵 → ∀ 𝑥 𝑤𝐵 )
13 3 12 bnj1307 ( 𝑤𝐶 → ∀ 𝑥 𝑤𝐶 )
14 13 nfcii 𝑥 𝐶
15 14 nfuni 𝑥 𝐶
16 4 15 nfcxfr 𝑥 𝐹
17 nfcv 𝑥 𝐻
18 16 17 nfne 𝑥 𝐹𝐻
19 11 18 nfan 𝑥 ( 𝜑𝐹𝐻 )
20 6 19 nfxfr 𝑥 𝜓
21 20 nf5ri ( 𝜓 → ∀ 𝑥 𝜓 )