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 35050

Description: Technical lemma for bnj1414 35051. 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 228	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜃)
3		bnj1408.1	. . . . 5 ⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
4	3	bnj1413 35049	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V)
5		simplll 775	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
6		bnj213 34896	. . . . . . . . . . 11 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴
7	6	sseli 3979	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → 𝑧 ∈ 𝐴)
8	7	adantl 481	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
9		bnj906 34944	. . . . . . . . 9 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
10	5, 8, 9	syl2anc 584	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
11		bnj1318 35039	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → trCl(𝑦, 𝐴, 𝑅) = trCl(𝑧, 𝐴, 𝑅))
12	11	ssiun2s 5048	. . . . . . . . . 10 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
13		ssun4 4181	. . . . . . . . . . 11 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
14	13, 3	sseqtrrdi 4025	. . . . . . . . . 10 ⊢ ( trCl(𝑧, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
15	12, 14	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
16	15	adantl 481	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
17	10, 16	sstrd 3994	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ pred(𝑋, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
18		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
19	18	bnj1405 34850	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 ∈ pred (𝑋, 𝐴, 𝑅)𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
20		biid 261	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) ↔ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
21		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)
22		nfcv 2905	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 pred(𝑋, 𝐴, 𝑅)
23		nfiu1 5027	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
24	22, 23	nfun 4170	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
25	3, 24	nfcxfr 2903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝐵
26	25	nfcri 2897	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
27	21, 26	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵)
28	23	nfcri 2897	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)
29	27, 28	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
30	29	nf5ri 2195	. . . . . . . . . 10 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∀𝑦(((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
31	19, 20, 30	bnj1521 34865	. . . . . . . . 9 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)))
32		simplll 775	. . . . . . . . . . . . 13 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
33	32	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴)
34		bnj1147 35008	. . . . . . . . . . . . 13 ⊢ trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐴
35		simp3 1139	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅))
36	34, 35	bnj1213 34812	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑧 ∈ 𝐴)
37	33, 36, 9	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑧, 𝐴, 𝑅))
38		simp2 1138	. . . . . . . . . . . . 13 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ pred(𝑋, 𝐴, 𝑅))
39	6, 38	bnj1213 34812	. . . . . . . . . . . 12 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → 𝑦 ∈ 𝐴)
40		bnj1125 35006	. . . . . . . . . . . 12 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
41	33, 39, 35, 40	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
42	37, 41	sstrd 3994	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ trCl(𝑦, 𝐴, 𝑅))
43		ssiun2 5047	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ pred(𝑋, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
44	43	3ad2ant2 1135	. . . . . . . . . . 11 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
45		ssun4 4181	. . . . . . . . . . . 12 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ ( pred(𝑋, 𝐴, 𝑅) ∪ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
46	45, 3	sseqtrrdi 4025	. . . . . . . . . . 11 ⊢ ( trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
47	44, 46	syl 17	. . . . . . . . . 10 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ 𝐵)
48	42, 47	sstrd 3994	. . . . . . . . 9 ⊢ (((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∧ 𝑦 ∈ pred(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
49	31, 48	bnj593 34759	. . . . . . . 8 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → ∃𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
50		nfcv 2905	. . . . . . . . . 10 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅)
51	50, 25	nfss 3976	. . . . . . . . 9 ⊢ Ⅎ𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵
52	51	nf5ri 2195	. . . . . . . 8 ⊢ ( pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵 → ∀𝑦 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
53	49, 52	bnj1397 34848	. . . . . . 7 ⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) ∧ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
54		simpr 484	. . . . . . . 8 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
55	3	bnj1138 34802	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐵 ↔ (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
56	54, 55	sylib 218	. . . . . . 7 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ pred(𝑋, 𝐴, 𝑅) ∨ 𝑧 ∈ ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)))
57	17, 53, 56	mpjaodan 961	. . . . . 6 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐵) → pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
58	57	ralrimiva 3146	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
59		df-bnj19 34711	. . . . 5 ⊢ ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑧 ∈ 𝐵 pred(𝑧, 𝐴, 𝑅) ⊆ 𝐵)
60	58, 59	sylibr 234	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo(𝐵, 𝐴, 𝑅))
61	3	bnj931 34784	. . . . 5 ⊢ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵
62	61	a1i 11	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
63		bnj1408.4	. . . 4 ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))
64	4, 60, 62, 63	syl3anbrc 1344	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜏)
65	1, 63	bnj1124 35002	. . 3 ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
66	2, 64, 65	syl2anc 584	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)
67		bnj906 34944	. . . . 5 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))
68		iunss1 5006	. . . . 5 ⊢ ( pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) → ∪ 𝑦 ∈ pred (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅))
69		unss2 4187	. . . . 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 4037	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ 𝐶)
73		biid 261	. . . 4 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
74		biid 261	. . . 4 ⊢ ((𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶) ↔ (𝐶 ∈ V ∧ TrFo(𝐶, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐶))
75	71, 73, 74	bnj1136 35011	. . 3 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐶)
76	72, 75	sseqtrrd 4021	. 2 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ trCl(𝑋, 𝐴, 𝑅))
77	66, 76	eqssd 4001	1 ⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ∪ cun 3949 ⊆ wss 3951 ∪ ciun 4991 predc-bnj14 34702 FrSe w-bnj15 34706 trClc-bnj18 34708 TrFow-bnj19 34710

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-reg 9632 ax-inf2 9681

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-om 7888 df-1o 8506 df-bnj17 34701 df-bnj14 34703 df-bnj13 34705 df-bnj15 34707 df-bnj18 34709 df-bnj19 34711

This theorem is referenced by: bnj1414 35051

W3C validator