Theorem bnj1053 35106

Description: Technical lemma for bnj69 35140. 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
bnj1053.1	⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
bnj1053.2	⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj1053.3	⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
bnj1053.4	⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
bnj1053.5	⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))
bnj1053.6	⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))
bnj1053.7	⊢ 𝐷 = (ω ∖ {∅})
bnj1053.8	⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
bnj1053.9	⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
bnj1053.10	⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))
bnj1053.37	⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))

Assertion

Ref	Expression
bnj1053	⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)

Distinct variable groups:   𝐴,𝑓,𝑖,𝑛,𝑦   𝑧,𝐴,𝑓,𝑖,𝑛   𝐵,𝑓,𝑖,𝑛,𝑧   𝐷,𝑖   𝑅,𝑓,𝑖,𝑛,𝑦   𝑧,𝑅   𝑓,𝑋,𝑖,𝑛,𝑦   𝑧,𝑋   𝜂,𝑗   𝜏,𝑓,𝑖,𝑛,𝑧   𝜃,𝑓,𝑖,𝑛,𝑧   𝑖,𝑗,𝑛   𝜑,𝑖

Allowed substitution hints:   𝜑(𝑦,𝑧,𝑓,𝑗,𝑛)   𝜓(𝑦,𝑧,𝑓,𝑖,𝑗,𝑛)   𝜒(𝑦,𝑧,𝑓,𝑖,𝑗,𝑛)   𝜃(𝑦,𝑗)   𝜏(𝑦,𝑗)   𝜂(𝑦,𝑧,𝑓,𝑖,𝑛)   𝜁(𝑦,𝑧,𝑓,𝑖,𝑗,𝑛)   𝜌(𝑦,𝑧,𝑓,𝑖,𝑗,𝑛)   𝐴(𝑗)   𝐵(𝑦,𝑗)   𝐷(𝑦,𝑧,𝑓,𝑗,𝑛)   𝑅(𝑗)   𝐾(𝑦,𝑧,𝑓,𝑖,𝑗,𝑛)   𝑋(𝑗)

Proof of Theorem bnj1053

Step	Hyp	Ref	Expression
1		bnj1053.1	. 2 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅))
2		bnj1053.2	. 2 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
3		bnj1053.3	. 2 ⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
4		bnj1053.4	. 2 ⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴))
5		bnj1053.5	. 2 ⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵))
6		bnj1053.6	. 2 ⊢ (𝜁 ↔ (𝑖 ∈ 𝑛 ∧ 𝑧 ∈ (𝑓‘𝑖)))
7		bnj1053.7	. 2 ⊢ 𝐷 = (ω ∖ {∅})
8		bnj1053.8	. 2 ⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)}
9		bnj1053.9	. 2 ⊢ (𝜂 ↔ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → 𝑧 ∈ 𝐵))
10		bnj1053.10	. 2 ⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂))
11	7	bnj923 34899	. . . . . 6 ⊢ (𝑛 ∈ 𝐷 → 𝑛 ∈ ω)
12		nnord 7814	. . . . . 6 ⊢ (𝑛 ∈ ω → Ord 𝑛)
13		ordfr 6327	. . . . . 6 ⊢ (Ord 𝑛 → E Fr 𝑛)
14	11, 12, 13	3syl 18	. . . . 5 ⊢ (𝑛 ∈ 𝐷 → E Fr 𝑛)
15	3, 14	bnj769 34893	. . . 4 ⊢ (𝜒 → E Fr 𝑛)
16	15	bnj707 34886	. . 3 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → E Fr 𝑛)
17		bnj1053.37	. . 3 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂))
18	16, 17	jca 511	. 2 ⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ( E Fr 𝑛 ∧ ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂)))
19	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 18	bnj1052 35105	1 ⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {cab 2713  ∀wral 3049  ∃wrex 3059  Vcvv 3427  [wsbc 3725   ∖ cdif 3882   ⊆ wss 3885  ∅c0 4263  {csn 4557  ∪ ciun 4923   class class class wbr 5074   E cep 5519   Fr wfr 5570  Ord word 6311  suc csuc 6314   Fn wfn 6482  ‘cfv 6487  ωcom 7806   ∧ w-bnj17 34817   predc-bnj14 34819   FrSe w-bnj15 34823   trClc-bnj18 34825   TrFow-bnj19 34827

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-iun 4925  df-br 5075  df-tr 5182  df-po 5528  df-so 5529  df-fr 5573  df-we 5575  df-ord 6315  df-on 6316  df-fn 6490  df-om 7807  df-bnj17 34818  df-bnj18 34826

This theorem is referenced by: (None)