bnj1018g

Description: Version of bnj1018 with less disjoint variable conditions, but requiring ax-13 . (Contributed by Gino Giotto, 27-Mar-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1018.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj1018.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj1018.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
	bnj1018.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
	bnj1018.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
	bnj1018.7	No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
	bnj1018.8	No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
	bnj1018.9	No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
	bnj1018.10	No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
	bnj1018.11	No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
	bnj1018.12	No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
	bnj1018.13	$⊢ D = ω ∖ \{\emptyset\}$
	bnj1018.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj1018.15	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
	bnj1018.16	$⊢ G = f \cup \{⟨n, C⟩\}$
	bnj1018.26	No typesetting found for \|- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode \|-
	bnj1018.29	No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode \|-
	bnj1018.30	No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode \|-
Assertion	bnj1018g	$⊢ (θ \land χ \land η \land \exists p τ) \to G (suc i) \subseteq trCl (X, A, R)$

Proof

Step	Hyp	Ref	Expression
1		bnj1018.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj1018.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj1018.3	$⊢ χ \leftrightarrow (n \in D \land f Fn n \land φ \land ψ)$
4		bnj1018.4	$⊢ θ \leftrightarrow (R FrSe A \land X \in A \land y \in trCl (X, A, R) \land z \in pred (y, A, R))$
5		bnj1018.5	$⊢ τ \leftrightarrow (m \in ω \land n = suc m \land p = suc n)$
6		bnj1018.7	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for \|- ( ph' <-> [. p / n ]. ph ) with typecode \|-
7		bnj1018.8	Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for \|- ( ps' <-> [. p / n ]. ps ) with typecode \|-
8		bnj1018.9	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for \|- ( ch' <-> [. p / n ]. ch ) with typecode \|-
9		bnj1018.10	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for \|- ( ph" <-> [. G / f ]. ph' ) with typecode \|-
10		bnj1018.11	Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for \|- ( ps" <-> [. G / f ]. ps' ) with typecode \|-
11		bnj1018.12	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for \|- ( ch" <-> [. G / f ]. ch' ) with typecode \|-
12		bnj1018.13	$⊢ D = ω ∖ \{\emptyset\}$
13		bnj1018.14	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
14		bnj1018.15	$⊢ C = ⋃_{y \in f (m)} pred (y, A, R)$
15		bnj1018.16	$⊢ G = f \cup \{⟨n, C⟩\}$
16		bnj1018.26	Could not format ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for \|- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode \|-
17		bnj1018.29	Could not format ( ( th /\ ch /\ ta /\ et ) -> ch" ) : No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode \|-
18		bnj1018.30	Could not format ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) : No typesetting found for \|- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode \|-
19		df-bnj17	$⊢ (θ \land χ \land η \land \exists p τ) \leftrightarrow ((θ \land χ \land η) \land \exists p τ)$
20		bnj258	$⊢ (θ \land χ \land τ \land η) \leftrightarrow ((θ \land χ \land η) \land τ)$
21	20 17	sylbir	Could not format ( ( ( th /\ ch /\ et ) /\ ta ) -> ch" ) : No typesetting found for \|- ( ( ( th /\ ch /\ et ) /\ ta ) -> ch" ) with typecode \|-
22	21	ex	Could not format ( ( th /\ ch /\ et ) -> ( ta -> ch" ) ) : No typesetting found for \|- ( ( th /\ ch /\ et ) -> ( ta -> ch" ) ) with typecode \|-
23	22	eximdv	Could not format ( ( th /\ ch /\ et ) -> ( E. p ta -> E. p ch" ) ) : No typesetting found for \|- ( ( th /\ ch /\ et ) -> ( E. p ta -> E. p ch" ) ) with typecode \|-
24	3 8 11 13 15	bnj985	Could not format ( G e. B <-> E. p ch" ) : No typesetting found for \|- ( G e. B <-> E. p ch" ) with typecode \|-
25	23 24	syl6ibr	$⊢ (θ \land χ \land η) \to (\exists p τ \to G \in B)$
26	25	imp	$⊢ ((θ \land χ \land η) \land \exists p τ) \to G \in B$
27	19 26	sylbi	$⊢ (θ \land χ \land η \land \exists p τ) \to G \in B$
28		bnj1019	$⊢ \exists p (θ \land χ \land τ \land η) \leftrightarrow (θ \land χ \land η \land \exists p τ)$
29	18	simp3d	$⊢ (θ \land χ \land τ \land η) \to suc i \in p$
30	16	bnj1235	Could not format ( ch" -> G Fn p ) : No typesetting found for \|- ( ch" -> G Fn p ) with typecode \|-
31		fndm	$⊢ G Fn p \to dom G = p$
32	17 30 31	3syl	$⊢ (θ \land χ \land τ \land η) \to dom G = p$
33	29 32	eleqtrrd	$⊢ (θ \land χ \land τ \land η) \to suc i \in dom G$
34	33	exlimiv	$⊢ \exists p (θ \land χ \land τ \land η) \to suc i \in dom G$
35	28 34	sylbir	$⊢ (θ \land χ \land η \land \exists p τ) \to suc i \in dom G$
36	15	bnj918	$⊢ G \in V$
37		vex	$⊢ i \in V$
38	37	sucex	$⊢ suc i \in V$
39	1 2 12 13 36 38	bnj1015	$⊢ (G \in B \land suc i \in dom G) \to G (suc i) \subseteq trCl (X, A, R)$
40	27 35 39	syl2anc	$⊢ (θ \land χ \land η \land \exists p τ) \to G (suc i) \subseteq trCl (X, A, R)$

Metamath Proof Explorer

Theorem bnj1018g

Proof