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 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1525.2 ⊢ Y = x f ↾ pred x A R
bnj1525.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj1525.4 ⊢ F = ⋃ C
bnj1525.5 ⊢ φ ↔ R FrSe A ∧ H Fn A ∧ ∀ x ∈ A H ⁡ x = G ⁡ x H ↾ pred x A R
bnj1525.6 ⊢ ψ ↔ φ ∧ F ≠ H
Assertion bnj1525 ⊢ ψ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 bnj1525.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1525.2 ⊢ Y = x f ↾ pred x A R
3 bnj1525.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1525.4 ⊢ F = ⋃ C
5 bnj1525.5 ⊢ φ ↔ R FrSe A ∧ H Fn A ∧ ∀ x ∈ A H ⁡ x = G ⁡ x H ↾ pred x A R
6 bnj1525.6 ⊢ ψ ↔ φ ∧ F ≠ H
7 nfv ⊢ Ⅎ x R FrSe A
8 nfv ⊢ Ⅎ x H Fn A
9 nfra1 ⊢ Ⅎ x ∀ x ∈ A H ⁡ x = G ⁡ x H ↾ pred x A R
10 7 8 9 nf3an ⊢ Ⅎ x R FrSe A ∧ H Fn A ∧ ∀ x ∈ A H ⁡ x = G ⁡ x H ↾ pred x A R
11 5 10 nfxfr ⊢ Ⅎ x φ
12 1 bnj1309 ⊢ w ∈ B → ∀ x w ∈ B
13 3 12 bnj1307 ⊢ w ∈ C → ∀ x w ∈ C
14 13 nfcii ⊢ Ⅎ _ x C
15 14 nfuni ⊢ Ⅎ _ x ⋃ C
16 4 15 nfcxfr ⊢ Ⅎ _ x F
17 nfcv ⊢ Ⅎ _ x H
18 16 17 nfne ⊢ Ⅎ x F ≠ H
19 11 18 nfan ⊢ Ⅎ x φ ∧ F ≠ H
20 6 19 nfxfr ⊢ Ⅎ x ψ
21 20 nf5ri ⊢ ψ → ∀ x ψ