Theorem bnj109 14155

Description: First-order logic and set theory.

Hypotheses

Ref	Expression
bnj109.1	|- (ph <-> (f` (/)) = pred(x, A, R))
bnj109.2	|- (ps <-> A.i e. om (suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)))
bnj109.3	|- F = {<.(/), pred(x, A, R)>.}

Assertion

Ref	Expression
bnj109	|- [F / f]((R FrSe A /\ x e. A) -> (f Fn 1o /\ [1o / n]ph /\ [1o / n]ps))

Distinct variable groups:   A,f,n,x   f,F,i,y   R,f,n,x   i,n,y

Proof of Theorem bnj109

Step	Hyp	Ref	Expression
1		bnj109.3	. . . . . . 7 |- F = {<.(/), pred(x, A, R)>.}
2	1	bnj103 14152	. . . . . 6 |- ((R FrSe A /\ x e. A) -> F Fn 1o)
3	1	bnj95 14147	. . . . . . 7 |- F e. _V
4	3	bnj99 13392	. . . . . 6 |- ([F / f]f Fn 1o <-> F Fn 1o)
5	2, 4	sylibr 264	. . . . 5 |- ((R FrSe A /\ x e. A) -> [F / f]f Fn 1o)
6	1	bnj97 14149	. . . . . 6 |- ((R FrSe A /\ x e. A) -> (F` (/)) = pred(x, A, R))
7		bnj109.1	. . . . . . 7 |- (ph <-> (f` (/)) = pred(x, A, R))
8	7, 3	bnj104 14153	. . . . . 6 |- ([F / f][1o / n]ph <-> (F` (/)) = pred(x, A, R))
9	6, 8	sylibr 264	. . . . 5 |- ((R FrSe A /\ x e. A) -> [F / f][1o / n]ph)
10	5, 9	jca 590	. . . 4 |- ((R FrSe A /\ x e. A) -> ([F / f]f Fn 1o /\ [F / f][1o / n]ph))
11		bnj98 14150	. . . . 5 |- A.i e. om (suc i e. 1o -> (F` suc i) = U_y e. (F` i) pred(y, A, R))
12		bnj109.2	. . . . . 6 |- (ps <-> A.i e. om (suc i e. n -> (f` suc i) = U_y e. (f` i) pred(y, A, R)))
13	12, 3	bnj106 14154	. . . . 5 |- ([F / f][1o / n]ps <-> A.i e. om (suc i e. 1o -> (F` suc i) = U_y e. (F` i) pred(y, A, R)))
14	11, 13	mpbir 255	. . . 4 |- [F / f][1o / n]ps
15	10, 14	jctir 598	. . 3 |- ((R FrSe A /\ x e. A) -> (([F / f]f Fn 1o /\ [F / f][1o / n]ph) /\ [F / f][1o / n]ps))
16		df-3an 1132	. . 3 |- (([F / f]f Fn 1o /\ [F / f][1o / n]ph /\ [F / f][1o / n]ps) <-> (([F / f]f Fn 1o /\ [F / f][1o / n]ph) /\ [F / f][1o / n]ps))
17	15, 16	sylibr 264	. 2 |- ((R FrSe A /\ x e. A) -> ([F / f]f Fn 1o /\ [F / f][1o / n]ph /\ [F / f][1o / n]ps))
18		sbcimg 2764	. . . 4 |- (F e. _V -> ([F / f]((R FrSe A /\ x e. A) -> (f Fn 1o /\ [1o / n]ph /\ [1o / n]ps)) <-> ([F / f](R FrSe A /\ x e. A) -> [F / f](f Fn 1o /\ [1o / n]ph /\ [1o / n]ps))))
19	3, 18	ax-mp 7	. . 3 |- ([F / f]((R FrSe A /\ x e. A) -> (f Fn 1o /\ [1o / n]ph /\ [1o / n]ps)) <-> ([F / f](R FrSe A /\ x e. A) -> [F / f](f Fn 1o /\ [1o / n]ph /\ [1o / n]ps)))
20		ax-17 1634	. . . . . 6 |- ((R FrSe A /\ x e. A) -> A.f(R FrSe A /\ x e. A))
21	20	sbcgf 2784	. . . . 5 |- (F e. _V -> ([F / f](R FrSe A /\ x e. A) <-> (R FrSe A /\ x e. A)))
22	3, 21	ax-mp 7	. . . 4 |- ([F / f](R FrSe A /\ x e. A) <-> (R FrSe A /\ x e. A))
23		sbc3ang 2777	. . . . 5 |- (F e. _V -> ([F / f](f Fn 1o /\ [1o / n]ph /\ [1o / n]ps) <-> ([F / f]f Fn 1o /\ [F / f][1o / n]ph /\ [F / f][1o / n]ps)))
24	3, 23	ax-mp 7	. . . 4 |- ([F / f](f Fn 1o /\ [1o / n]ph /\ [1o / n]ps) <-> ([F / f]f Fn 1o /\ [F / f][1o / n]ph /\ [F / f][1o / n]ps))
25	22, 24	imbi12i 376	. . 3 |- (([F / f](R FrSe A /\ x e. A) -> [F / f](f Fn 1o /\ [1o / n]ph /\ [1o / n]ps)) <-> ((R FrSe A /\ x e. A) -> ([F / f]f Fn 1o /\ [F / f][1o / n]ph /\ [F / f][1o / n]ps)))
26	19, 25	bitri 306	. 2 |- ([F / f]((R FrSe A /\ x e. A) -> (f Fn 1o /\ [1o / n]ph /\ [1o / n]ps)) <-> ((R FrSe A /\ x e. A) -> ([F / f]f Fn 1o /\ [F / f][1o / n]ph /\ [F / f][1o / n]ps)))
27	17, 26	mpbir 255	1 |- [F / f]((R FrSe A /\ x e. A) -> (f Fn 1o /\ [1o / n]ph /\ [1o / n]ps))

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617  [wsbc 1843  A.wral 2385  _Vcvv 2569  (/)c0 3114  {csn 3270  <.cop 3272  U_ciun 3468  suc csuc 3845  omcom 4117   Fn wfn 4158  ` cfv 4163  1oc1o 5379   predsyn-bnj14 13012   FrSe syn-bnj15 13016

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-v 2571  df-sbc 2731  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-iun 3470  df-br 3540  df-opab 3598  df-id 3779  df-suc 3849  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-fv 4179  df-1o 5384  df-bnj13 13015  df-bnj15 13017

Copyright terms: Public domain