bnj1408 - Mathbox for Jonathan Ben-Naim

	Mathbox for Jonathan Ben-Naim		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj1408		Structured version Visualization version GIF version

Theorem bnj1408 32310

Description: Technical lemma for bnj1414 32311. 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.)

**Hypotheses**
Ref	Expression
bnj1408.1	⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
bnj1408.2	⊢ 𝐶 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
bnj1408.3	⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
bnj1408.4	⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))

**Assertion**
Ref	Expression
bnj1408	⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)

Distinct variable groups: 𝑦,𝐴 𝑦,𝑅 𝑦,𝑋 Allowed substitution hints: 𝜃(𝑦) 𝜏(𝑦) 𝐵(𝑦) 𝐶(𝑦)

Proof of Theorem bnj1408 Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bnj1408.3	. . . 4 ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
2	1	biimpri 230	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜃)
3		bnj1408.1	. . . . 5 ⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
4	3	bnj1413 32309	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)
5		simplll 773	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
6		bnj213 32156	. . . . . . . . . . 11 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
7	6	sseli 3965	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → 𝑧 ∈ 𝐴)
8	7	adantl 484	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
9		bnj906 32204	. . . . . . . . 9 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
10	5, 8, 9	syl2anc 586	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
11		bnj1318 32299	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → trCl(𝑦, 𝐴, 𝑅) = trCl(𝑧, 𝐴, 𝑅))
12	11	ssiun2s 4974	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
13		ssun4 4153	. . . . . . . . . . 11 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
14	13, 3	sseqtrrdi 4020	. . . . . . . . . 10 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
15	12, 14	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
16	15	adantl 484	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
17	10, 16	sstrd 3979	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
18		simpr 487	. . . . . . . . . . 11 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
19	18	bnj1405 32110	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 ∈ pred (𝑋, 𝐴, 𝑅)𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
20		biid 263	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) ↔ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
21		nfv 1915	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)
22		nfcv 2979	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 pred(𝑋, 𝐴, 𝑅)
23		nfiu1 4955	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
24	22, 23	nfun 4143	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
25	3, 24	nfcxfr 2977	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
26	25	nfcri 2973	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
27	21, 26	nfan 1900	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵)
28	23	nfcri 2973	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
29	27, 28	nfan 1900	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
30	29	nf5ri 2195	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∀𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
31	19, 20, 30	bnj1521 32125	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
32		simplll 773	. . . . . . . . . . . . 13 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
33	32	3ad2ant1 1129	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
34		bnj1147 32268	. . . . . . . . . . . . 13 ⊢ trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴
35		simp3 1134	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
36	34, 35	bnj1213 32072	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
37	33, 36, 9	syl2anc 586	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
38		simp2 1133	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ pred(𝑋, 𝐴, 𝑅))
39	6, 38	bnj1213 32072	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ 𝐴)
40		bnj1125 32266	. . . . . . . . . . . 12 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
41	33, 39, 35, 40	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
42	37, 41	sstrd 3979	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
43		ssiun2 4973	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
44	43	3ad2ant2 1130	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
45		ssun4 4153	. . . . . . . . . . . 12 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
46	45, 3	sseqtrrdi 4020	. . . . . . . . . . 11 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
47	44, 46	syl 17	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
48	42, 47	sstrd 3979	. . . . . . . . 9 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
49	31, 48	bnj593 32018	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
50		nfcv 2979	. . . . . . . . . 10 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅)
51	50, 25	nfss 3962	. . . . . . . . 9 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵
52	51	nf5ri 2195	. . . . . . . 8 ⊢ ( pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵 → ∀𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
53	49, 52	bnj1397 32108	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
54		simpr 487	. . . . . . . 8 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
55	3	bnj1138 32062	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↔ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
56	54, 55	sylib 220	. . . . . . 7 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
57	17, 53, 56	mpjaodan 955	. . . . . 6 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
58	57	ralrimiva 3184	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
59		df-bnj19 31969	. . . . 5 ⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
60	58, 59	sylibr 236	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo(𝐵, 𝐴, 𝑅))
61	3	bnj931 32044	. . . . 5 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵
62	61	a1i 11	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
63		bnj1408.4	. . . 4 ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))
64	4, 60, 62, 63	syl3anbrc 1339	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜏)
65	1, 63	bnj1124 32262	. . 3 ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
66	2, 64, 65	syl2anc 586	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
67		bnj906 32204	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
68		iunss1 4935	. . . . 5 ⊢ ( pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) → ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
69		unss2 4159	. . . . 5 ⊢ (∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
70	67, 68, 69	3syl 18	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
71		bnj1408.2	. . . 4 ⊢ 𝐶 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
72	70, 3, 71	3sstr4g 4014	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ 𝐶)
73		biid 263	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
74		biid 263	. . . 4 ⊢ ((𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶) ↔ (𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶))
75	71, 73, 74	bnj1136 32271	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐶)
76	72, 75	sseqtrrd 4010	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ trCl(𝑋, 𝐴, 𝑅))
77	66, 76	eqssd 3986	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ∀wral 3140 Vcvv 3496 ∪ cun 3936 ⊆ wss 3938 ∪ ciun 4921 predc-bnj14 31960 FrSe w-bnj15 31964 trClc-bnj18 31966 TrFow-bnj19 31968

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-reg 9058 ax-inf2 9106

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-ral 3145 df-rex 3146 df-reu 3147 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-om 7583 df-1o 8104 df-bnj17 31959 df-bnj14 31961 df-bnj13 31963 df-bnj15 31965 df-bnj18 31967 df-bnj19 31969

This theorem is referenced by: bnj1414 32311

W3C validator